diff options
| author | courtieu | 2012-07-21 12:30:22 +0000 |
|---|---|---|
| committer | courtieu | 2012-07-21 12:30:22 +0000 |
| commit | 2db51f012e1276f15391e7ef44a2db5724cd3583 (patch) | |
| tree | 081a1a120ae1ae17393cfec9bfdd9b7c0cc3f6fd | |
| parent | 57128547546baa38ab436c87ed66361342c36cb8 (diff) | |
Slight modification to the printing of goals when in emacs mode.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15635 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | printing/printer.ml | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index a820f997a2..14d909f88f 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -356,6 +356,8 @@ let emacs_print_dependent_evars sigma seeds = (* spiwack: [seeds] is for printing dependent evars in emacs mode. *) (* spiwack: [pr_first] is true when the first goal must be singled out and printed in its entirety. *) +(* courtieu: in emacs mode, even less cases where the first goal is printed + in its entirety *) let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals = let rec print_stack a = function | [] -> Pp.int a @@ -397,13 +399,13 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals = ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++ str "You can use Grab Existential Variables.") end - | [g],[] -> + | [g],[] when not !Flags.print_emacs -> let pg = default_pr_goal { it = g ; sigma = sigma } in v 0 ( str "1 subgoal" ++ pr_goal_tag g ++ cut () ++ pg ++ emacs_print_dependent_evars sigma seeds ) - | [g],a::l -> + | [g],a::l when not !Flags.print_emacs -> let pg = default_pr_goal { it = g ; sigma = sigma } in v 0 ( str "1 focused subgoal (" ++ print_unfocused a l ++ str")" ++ pr_goal_tag g ++ cut () ++ pg @@ -467,7 +469,12 @@ let pr_open_subgoals () = | [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in begin match bgoals with | [] -> pr_subgoals None sigma seeds stack goals - | _ -> str"This subproof is complete, but there are still unfocused goals." ++ fnl () ++ fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds [] bgoals + | _ -> + (* emacs mode: xml-like flag for detecting information message *) + str (emacs_str "<infomsg>") ++ + str "This subproof is complete, but there are still unfocused goals." + ++ str (emacs_str "</infomsg>") + ++ fnl () ++ fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds [] bgoals end | _ -> pr_subgoals None sigma seeds stack goals end |