-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathemacs_commands.ml
93 lines (75 loc) · 3.1 KB
/
emacs_commands.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
(*
* prooftree --- proof tree display for Proof General
*
* Copyright (C) 2011 - 2024 Hendrik Tews
*
* This file is part of "prooftree".
*
* "prooftree" is free software: you can redistribute it and/or
* modify it under the terms of the GNU General Public License as
* published by the Free Software Foundation, either version 3 of the
* License, or (at your option) any later version.
*
* "prooftree" is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
* General Public License in file COPYING in this or one of the parent
* directories for more details.
*
* You should have received a copy of the GNU General Public License
* along with "prooftree". If not, see <http://www.gnu.org/licenses/>.
*)
(** Generate and output emacs callback requests *)
(* needed only for debug printing
* open Util
*)
(* sends 14 chars + cmd *)
(* XXX assert that the whole command, including both newlines, are
less than PIPE_BUF bytes, get the latter from configure and getconf
-a, getconf PIPE_BUF does not work.
Similarly for the complete first line, including both newlines, of
emacs_long_callback.
Neet to include both newlines, because PG pattern matches on both.
*)
(** Print [cmd] as emacs callback command. *)
let emacs_callback cmd =
(* Printf.fprintf (debugc()) "<- %s\n%!" cmd; *)
Printf.printf "\nemacs exec: %s\n%!" cmd
(** Print [cmd] as emacs callback command with a long data section. *)
let emacs_long_callback cmd data =
Printf.printf "\nemacs exec: %s %d\n%s\n%!" cmd (String.length data) data
(*
* let emacs_long_callback cmd data =
* Printf.printf "\nemacs exec: %s %d\n%s%!" cmd (String.length data)
* (String.sub data 0 2);
* Unix.sleep 1;
* Printf.printf "%s%!" (String.sub data 2 4);
* Unix.sleep 1;
* Printf.printf "%s\n%!" (String.sub data 4 (String.length data - 4))
*)
(** Issue the stop-displaying emacs callback command. *)
let emacs_callback_stop_display () =
emacs_callback "stop-displaying"
(** Send an undo command to emacs. *)
let emacs_callback_undo undo_state =
emacs_callback (Printf.sprintf "undo %d" undo_state)
(** Send a piece of proof script to Proof General. *)
let emacs_send_proof_script script =
emacs_long_callback "insert-proof-script" script
(* 23 chars + goal_id + state + proof_name *)
(** Request Show Goal <ID> at <state> from PG. The proof name is
needed to associate the output with a proof, because the command
can be delayed arbitrarily.
*)
let emacs_send_show_goal proof_name state goal_id =
(* Printf.fprintf (debugc()) "emacsrequest goal %s at state %d\n%!"
* goal_id state;
*)
emacs_callback (Printf.sprintf "show-goal \"%s\" at %d for \"%s\""
goal_id state proof_name)
(** Send [confirm-proof_complete] that tells PG that no more show goal
commands will follow.
*)
let emacs_confirm_proof_complete proof_name =
(* Printf.fprintf (debugc()) "emacs_confirm_proof_complete\n%!"; *)
emacs_callback (Printf.sprintf "confirm-proof-complete \"%s\"" proof_name)