diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-08 18:52:17 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-08 18:52:17 +0000 |
| commit | b213bae73ca927874275a896482246b2ee761b7b (patch) | |
| tree | 5320ce95e65b3474ba7a43a43ba1d49c21216310 /toplevel | |
| parent | a936e9ae133f103ed9f781a7aa363c0006a2f178 (diff) | |
Support Proof General
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16678 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/stm.ml | 8 | ||||
| -rw-r--r-- | toplevel/toplevel.ml | 16 | ||||
| -rw-r--r-- | toplevel/vernac_classifier.ml | 1 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 1 |
4 files changed, 25 insertions, 1 deletions
diff --git a/toplevel/stm.ml b/toplevel/stm.ml index a6d120d5c..c1376079e 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -831,6 +831,14 @@ let process_transaction verbosely (loc, expr) = | VtUnknown, VtLater -> anomaly(str"classifier: VtUnknown must imply VtNow") end; + (* Proof General *) + begin match v with + | VernacStm (PGLast _) -> + if head <> VCS.master then + interp dummy_state_id + (true,Loc.ghost,VernacShow (ShowGoal OpenSubgoals)) + | _ -> () + end; prerr_endline "executed }}}"; VCS.print () with e -> diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index dcf2b0b3d..eb9f4a03d 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -306,7 +306,9 @@ let do_vernac () = msgerrnl (mt ()); if !print_emacs then msgerr (str (top_buffer.prompt())); resynch_buffer top_buffer; - try Vernac.eval_expr (read_sentence ()); Stm.finish () + try + Vernac.eval_expr (read_sentence ()); + if not !Flags.print_emacs then Stm.finish () with | End_of_input | Errors.Quit -> msgerrnl (mt ()); pp_flush(); raise Errors.Quit @@ -331,8 +333,20 @@ let do_vernac () = exit the loop are Drop and Quit. Any other exception there indicates an issue with [print_toplevel_error] above. *) +let feed_emacs = function + | { Interface.id = Interface.State id; + Interface.content = Interface.GlobRef (_,a,_,c,_) } -> + prerr_endline ("<info>" ^"<id>"^Stateid.string_of_state_id id ^"</id>" + ^a^" "^c^ "</info>") + | _ -> () + let rec loop () = Sys.catch_break true; + if !Flags.print_emacs then begin + Pp.set_feeder feed_emacs; + Vernacentries.enable_goal_printing := false; + Vernacentries.qed_display_script := false; + end; try reset_input_buffer stdin top_buffer; while true do do_vernac(); flush_all() done diff --git a/toplevel/vernac_classifier.ml b/toplevel/vernac_classifier.ml index d7b9553a0..46e04d87e 100644 --- a/toplevel/vernac_classifier.ml +++ b/toplevel/vernac_classifier.ml @@ -50,6 +50,7 @@ let rec classify_vernac e = | VernacStm JoinDocument -> VtStm (VtJoinDocument, true), VtNow | VernacStm (Observe id) -> VtStm (VtObserve id, true), VtNow | VernacStm (Command x) -> elide_part_of_script_and_now (classify_vernac x) + | VernacStm (PGLast x) -> fst (classify_vernac x), VtNow (* Impossible, Vernac handles these *) | VernacList _ -> anomaly (str "VernacList not handled by Vernac") | VernacLoad _ -> anomaly (str "VernacLoad not handled by Vernac") diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 706b757db..5316e9d46 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1814,6 +1814,7 @@ let interp ?(verbosely=true) ?proof (loc,c) = | VernacLocal (b, c) when locality = None -> aux ~locality:b isprogcmd c | VernacLocal _ -> Errors.error "Locality specified twice" | VernacStm (Command c) -> aux ?locality isprogcmd c + | VernacStm (PGLast c) -> aux ?locality isprogcmd c | VernacStm _ -> assert false (* Done by Stm *) | VernacFail v -> begin try |