aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/coq.ml31
-rw-r--r--ide/coq.mli2
-rw-r--r--ide/coqide.ml58
-rw-r--r--ide/highlight.mll126
-rw-r--r--ide/ideutils.ml6
-rw-r--r--ide/ideutils.mli1
-rw-r--r--ide/preferences.ml2
7 files changed, 135 insertions, 91 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index aef993be65..41a6abad44 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -112,7 +112,7 @@ let user_error_loc l s =
type command_attribute =
NavigationCommand | QueryCommand | DebugCommand
- | OtherStatePreservingCommand | GoalStartingCommand
+ | OtherStatePreservingCommand | GoalStartingCommand | SolveCommand
let rec attribute_of_vernac_command = function
(* Control *)
@@ -167,8 +167,8 @@ let rec attribute_of_vernac_command = function
| VernacDeclareInstance _ -> []
(* Solving *)
- | VernacSolve _ -> []
- | VernacSolveExistential _ -> []
+ | VernacSolve _ -> [SolveCommand]
+ | VernacSolveExistential _ -> [SolveCommand]
(* MMode *)
| VernacDeclProof -> []
@@ -243,6 +243,7 @@ let rec attribute_of_vernac_command = function
| VernacToplevelControl _ -> []
(* Extensions *)
+ | VernacExtend ("Subtac_Obligations", _) -> [GoalStartingCommand]
| VernacExtend _ -> []
let is_vernac_goal_starting_command com =
@@ -257,18 +258,18 @@ let is_vernac_query_command com =
let is_vernac_debug_command com =
List.mem DebugCommand (attribute_of_vernac_command com)
+let is_vernac_goal_printing_command com =
+ let attribute = attribute_of_vernac_command com in
+ List.mem GoalStartingCommand attribute or
+ List.mem SolveCommand attribute
+
let is_vernac_state_preserving_command com =
let attribute = attribute_of_vernac_command com in
- let b =
- List.mem OtherStatePreservingCommand attribute or
- List.mem QueryCommand attribute in
- if b then prerr_endline "state preserving command found";
- b
-
-let rec is_tactic = function
- | VernacSolve _ -> true
- | VernacTime com -> is_tactic com
- | _ -> false
+ List.mem OtherStatePreservingCommand attribute or
+ List.mem QueryCommand attribute
+
+let is_vernac_tactic_command com =
+ List.mem SolveCommand (attribute_of_vernac_command com)
let interp verbosely s =
prerr_endline "Starting interp...";
@@ -287,7 +288,9 @@ let interp verbosely s =
if is_vernac_query_command vernac then
!flash_info
"Warning: query commands should not be inserted in scripts";
- Flags.make_silent (not verbosely); (*verbose if in small step forward*)
+ if not (is_vernac_goal_printing_command vernac) then
+ (* Verbose if in small step forward and not a tactic *)
+ Flags.make_silent (not verbosely);
Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s));
Flags.make_silent true;
prerr_endline ("...Done with interp of : "^s);
diff --git a/ide/coq.mli b/ide/coq.mli
index 32a62c2306..9c8e273200 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -20,7 +20,7 @@ val interp : bool -> string -> Util.loc * Vernacexpr.vernac_expr
val interp_last : Util.loc * Vernacexpr.vernac_expr -> unit
val interp_and_replace : string -> (Util.loc * Vernacexpr.vernac_expr) * string
-val is_tactic : Vernacexpr.vernac_expr -> bool
+val is_vernac_tactic_command : Vernacexpr.vernac_expr -> bool
val is_vernac_state_preserving_command : Vernacexpr.vernac_expr -> bool
val is_vernac_goal_starting_command : Vernacexpr.vernac_expr -> bool
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 29b55da6aa..1e6892d0d6 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -159,7 +159,7 @@ object('self)
method activate : unit -> unit
method active_keypress_handler : GdkEvent.Key.t -> bool
method backtrack_to : GText.iter -> unit
- method backtrack_to_no_lock : GText.iter -> unit
+ method backtrack_to_no_lock : GText.iter -> Names.identifier list -> unit
method clear_message : unit
method deactivate : unit -> unit
method disconnected_keypress_handler : GdkEvent.Key.t -> bool
@@ -1271,22 +1271,34 @@ object(self)
self#clear_message)();
Coq.reset_initial ()
-
(* backtrack Coq to the phrase preceding iterator [i] *)
- method backtrack_to_no_lock i =
+ method backtrack_to_no_lock i oldest_id_to_reset =
prerr_endline "Backtracking_to iter starts now.";
+ let was_refining = Pfedit.refining () in
(* re-synchronize Coq to the current state of the stack *)
- let rec synchro () =
+ let rec synchro oldest_decl_in_middle_of_proof =
if is_empty () then
Coq.reset_initial ()
else begin
let t = pop () in
begin match t.reset_info with
- | ResetAtSegmentStart (id, ({contents=true} as v)) ->
- v:=false; reset_to_mod id
- | ResetAtDecl (id, ({contents=true} as v)) ->
- v:=false; reset_to id
- | _ -> synchro ()
+ | ResetAtSegmentStart (id, {contents=true}) ->
+ reset_to_mod id
+ | ResetAtDecl (id, {contents=true}) ->
+ if was_refining then
+ (prerr_endline ("Skipping "^Names.string_of_id id);
+ synchro [id])
+ else
+ reset_to (List.hd (oldest_decl_in_middle_of_proof@[id]))
+ | ResetAtDecl (id, {contents=false}) ->
+ if was_refining then
+ (*reset oldest decl found before theorem started, if any*)
+ List.iter reset_to oldest_decl_in_middle_of_proof
+ else
+ (prerr_endline ("Skipping "^Names.string_of_id id);
+ synchro [id])
+ | _ ->
+ synchro oldest_decl_in_middle_of_proof
end;
interp_last t.ast;
repush_phrase t
@@ -1301,9 +1313,12 @@ object(self)
else
let t = top () in
if i#compare (input_buffer#get_iter_at_mark t.stop) < 0 then begin
+ prerr_endline "Popped top command";
ignore (pop ());
- let undos = if is_tactic (snd t.ast) then add_undo undos else None in
- pop_commands true undos
+ let undos =
+ if is_vernac_tactic_command (snd t.ast) then add_undo undos
+ else None in
+ pop_commands true undos
end else
done_smthg, undos
in
@@ -1313,8 +1328,8 @@ object(self)
begin
try
(match undos with
- | None -> synchro ()
- | Some n -> try Pfedit.undo n with _ -> synchro ());
+ | None -> synchro oldest_id_to_reset
+ | Some n -> try Pfedit.undo n with _ -> synchro oldest_id_to_reset);
sync (fun _ ->
let start =
if is_empty () then input_buffer#start_iter
@@ -1342,7 +1357,8 @@ Please restart and report NOW.";
method backtrack_to i =
if Mutex.try_lock coq_may_stop then
- (!push_info "Undoing...";self#backtrack_to_no_lock i ; Mutex.unlock coq_may_stop;
+ (!push_info "Undoing...";
+ self#backtrack_to_no_lock i []; Mutex.unlock coq_may_stop;
!pop_info ())
else prerr_endline "backtrack_to : discarded (lock is busy)"
@@ -1381,7 +1397,7 @@ Please restart and report NOW.";
| {ast=_, (VernacSolve _ | VernacTime (VernacSolve _))} ->
begin
try Pfedit.undo 1; ignore (pop ()); sync update_input ()
- with _ -> self#backtrack_to_no_lock start
+ with _ -> self#backtrack_to_no_lock start []
end
| {reset_info=ResetAtSegmentStart (id, {contents=true})} ->
@@ -1389,9 +1405,10 @@ Please restart and report NOW.";
reset_to_mod id;
sync update_input ()
| {reset_info=ResetAtDecl (id, {contents=true})} ->
- ignore (pop ());
- reset_to id;
- sync update_input ()
+ if Pfedit.refining () then
+ self#backtrack_to_no_lock start [id]
+ else
+ (ignore (pop ()); sync update_input ())
| {reset_info=ResetAtDecl (id,{contents=false})} ->
ignore (pop ());
(try
@@ -1406,7 +1423,7 @@ Please restart and report NOW.";
ignore (pop ());
sync update_input ()
| _ ->
- self#backtrack_to_no_lock start
+ self#backtrack_to_no_lock start []
end;
with
| Size 0 -> (* !flash_info "Nothing to Undo"*)()
@@ -3468,6 +3485,7 @@ let start () =
else failwith ("Coqide internal error: " ^ msg)));
Command_windows.main ();
Blaster_window.main 9;
+ init_stdout ();
main files;
if !Coq_config.with_geoproof then ignore (Thread.create check_for_geoproof_input ());
while true do
@@ -3480,5 +3498,3 @@ let start () =
flush stderr;
crash_save 127
done
-
-
diff --git a/ide/highlight.mll b/ide/highlight.mll
index 79b4e25aa7..6649dc31a7 100644
--- a/ide/highlight.mll
+++ b/ide/highlight.mll
@@ -18,18 +18,15 @@
let comment_start = ref 0
- let is_keyword =
+ (* Without this table, the automaton would be too big and
+ ocamllex would fail *)
+ let is_one_word_command =
let h = Hashtbl.create 97 in
List.iter (fun s -> Hashtbl.add h s ())
- [ "Add" ; "Check"; "Defined" ;
- "End" ; "Eval"; "Export" ; "Extraction" ; "Hint" ; "Hints" ;
- "Implicits" ; "Import" ;
- "Infix" ; "Load" ; "Module" ;
- "Notation"; "Proof" ; "Print"; "Qed" ;
- "Require" ; "Reset"; "Undo"; "Save" ;
- "Section" ; "Unset" ;
- "Set" ; "Notation";
- "Implicit"; "Arguments"; "Unfold"; "Resolve"
+ [ "Add" ; "Check"; "Eval"; "Extraction" ;
+ "Load" ; "Undo";
+ "Proof" ; "Print"; "Qed" ; "Defined" ; "Save" ;
+ "End" ; "Section"
];
Hashtbl.mem h
@@ -38,20 +35,31 @@
List.iter (fun s -> Hashtbl.add h s ())
[ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "for";
"end"; "as"; "let"; "in"; "dest"; "if"; "then"; "else"; "return";
- "Prop"; "Set"; "Type"];
+ "Prop"; "Set"; "Type" ];
Hashtbl.mem h
- let is_declaration =
+ (* Without this table, the automaton would be too big and
+ ocamllex would fail *)
+ let is_one_word_declaration =
let h = Hashtbl.create 97 in
List.iter (fun s -> Hashtbl.add h s ())
- [ "Theorem" ; "Lemma" ; "Fact" ; "Remark" ; "Corollary" ; "Proposition" ; "Property" ;
- "Definition" ; "Let" ; "Example" ; "SubClass" ; "Inductive" ; "CoInductive" ;
- "Record" ; "Structure" ; "Fixpoint" ; "CoFixpoint";
+ [ (* Theorems *)
+ "Theorem" ; "Lemma" ; "Fact" ; "Remark" ; "Corollary" ;
+ "Proposition" ; "Property" ;
+ (* Definitions *)
+ "Definition" ; "Let" ; "Example" ; "SubClass" ;
+ "Fixpoint" ; "CoFixpoint";
+ (* Assumptions *)
"Hypothesis" ; "Variable" ; "Axiom" ; "Parameter" ; "Conjecture" ;
- "Hypotheses" ; "Variables" ; "Axioms" ; "Parameters"
+ "Hypotheses" ; "Variables" ; "Axioms" ; "Parameters";
+ (* Inductive *)
+ "Inductive" ; "CoInductive" ; "Record" ; "Structure" ;
+ (* Other *)
+ "Ltac" ; "Typeclasses"; "Instance"
];
Hashtbl.mem h
+ let starting = ref true
}
let space =
@@ -62,44 +70,54 @@ let identchar =
['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9']
let ident = firstchar identchar*
-let thm_token = "Theorem" | "Lemma" | "Fact" | "Remark" | "Corollary" | "Proposition" | "Property"
-
-let def_token = "Definition" | "Let" | "Example" | "SubClass"
-
-let assumption = "Hypothesis" | "Variable" | "Axiom" | "Parameter" | "Conjecture" |
- "Hypotheses" | "Variables" | "Axioms" | "Parameters"
-
-let declaration =
- "Theorem" | "Lemma" | "Fact" | "Remark" | "Corollary" | "Proposition" | "Property" |
- "Definition" | "Let" | "Example" | "SubClass" |
- "Inductive" | "CoInductive" |
- "Record" | "Structure" |
- "Fixpoint" | "CoFixpoint"
-
+let multiword_declaration =
+ "Module" (space+ "Type")
+| "Program" space+ ident
+
+let locality = ("Local" space+)?
+
+let multiword_command =
+ "Set" (space+ ident)*
+| "Unset" (space+ ident)*
+| "Open" space+ locality "Scope"
+| "Next" space+ "Obligation"
+| "Solve" space+ "Obligations"
+| "Require" space+ ("Import"|"Export")
+| "Infix" space+ locality
+| "Notation" space+ locality
+| "Hint" space+ locality ident
+| "Reset" (space+ "Initial")?
+| "Tactic" space+ "Notation"
+
+rule next_starting_order = parse
+ | "(*" { comment_start := lexeme_start lexbuf; comment lexbuf }
+ | space+ { next_starting_order lexbuf }
+ | multiword_declaration
+ { starting:=false; lexeme_start lexbuf, lexeme_end lexbuf, "decl" }
+ | multiword_command
+ { starting:=false; lexeme_start lexbuf, lexeme_end lexbuf, "kwd" }
+ | ident as id
+ { starting:=false;
+ if is_one_word_command id then
+ lexeme_start lexbuf, lexeme_end lexbuf, "kwd"
+ else if is_one_word_declaration id then
+ lexeme_start lexbuf, lexeme_end lexbuf, "decl"
+ else
+ next_interior_order lexbuf
+ }
+ | _ { starting := false; next_interior_order lexbuf}
+ | eof { raise End_of_file }
-rule next_order = parse
+and next_interior_order = parse
| "(*"
{ comment_start := lexeme_start lexbuf; comment lexbuf }
- | "Module Type"
- { lexeme_start lexbuf, lexeme_end lexbuf, "kwd" }
- | "Program" space+ ident { lexeme_start lexbuf, lexeme_end lexbuf, "decl" }
| ident as id
- { if is_keyword id then
- lexeme_start lexbuf, lexeme_end lexbuf, "kwd"
- else
- begin
- if is_constr_kw id then
- lexeme_start lexbuf, lexeme_end lexbuf, "kwd"
- else
- begin
- if is_declaration id then
- lexeme_start lexbuf, lexeme_end lexbuf, "decl"
- else
- next_order lexbuf
- end
- end
- }
- | _ { next_order lexbuf}
+ { if is_constr_kw id then
+ lexeme_start lexbuf, lexeme_end lexbuf, "kwd"
+ else
+ next_interior_order lexbuf }
+ | "." (" "|"\n"|"\t") { starting := true; next_starting_order lexbuf }
+ | _ { next_interior_order lexbuf}
| eof { raise End_of_file }
and comment = parse
@@ -114,6 +132,7 @@ and comment = parse
let highlighting = ref false
let highlight_slice (input_buffer:GText.buffer) (start:GText.iter) stop =
+ starting := true; (* approximation: assume the beginning of a sentence *)
if !highlighting then prerr_endline "Rejected highlight"
else begin
highlighting := true;
@@ -130,7 +149,10 @@ and comment = parse
let lb = Lexing.from_string s in
try
while true do
- let b,e,o=next_order lb in
+ let b,e,o =
+ if !starting then next_starting_order lb
+ else next_interior_order lb in
+
let b,e = convert_pos b,convert_pos e in
let start = input_buffer#get_iter_at_char (offset + b) in
let stop = input_buffer#get_iter_at_char (offset + e) in
@@ -142,7 +164,7 @@ and comment = parse
highlighting := false
end
- let highlight_current_line input_buffer =
+ let highlight_current_line input_buffer =
try
let i = get_insert input_buffer in
highlight_slice input_buffer (i#set_line_offset 0) i
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index f4fd73d6fd..a3fd090840 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -148,13 +148,15 @@ let set_highlight_timer f =
(* Get back the standard coq out channels *)
-let read_stdout,clear_stdout =
+let init_stdout,read_stdout,clear_stdout =
let out_buff = Buffer.create 100 in
let out_ft = Format.formatter_of_buffer out_buff in
+ (fun () ->
Pp_control.std_ft := out_ft;
- Pp_control.err_ft := out_ft;
+ Pp_control.err_ft := out_ft),
(fun () -> Format.pp_print_flush out_ft ();
let r = Buffer.contents out_buff in
+ prerr_endline "Output from Coq is: "; prerr_endline r;
Buffer.clear out_buff; r),
(fun () ->
Format.pp_print_flush out_ft (); Buffer.clear out_buff)
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 5dad5b18b1..6b8307fc59 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -17,6 +17,7 @@ val mutex : string -> ('a -> unit) -> 'a -> unit
val browse : (string -> unit) -> string -> unit
val browse_keyword : (string -> unit) -> string -> unit
val byte_offset_to_char_offset : string -> int -> int
+val init_stdout : unit -> unit
val clear_stdout : unit -> unit
val debug : bool ref
val disconnect_revert_timer : unit -> unit
diff --git a/ide/preferences.ml b/ide/preferences.ml
index aeaeb4ec17..daca874add 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -276,7 +276,7 @@ let load_pref () =
set_bool "opposite_tabs" (fun v -> np.opposite_tabs <- v);
current := np;
(*
- Format.printf "in laod_pref: current.text_font = %s@." (Pango.Font.to_string !current.text_font);
+ Format.printf "in load_pref: current.text_font = %s@." (Pango.Font.to_string !current.text_font);
*)
with e ->
prerr_endline ("Could not load preferences ("^
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 01:41:00 +0000