From d8cc0ec7d99cc5f26b432b6ded95467064456ebf Mon Sep 17 00:00:00 2001 From: courtieu Date: Sun, 18 Dec 2011 20:17:49 +0000 Subject: Applied patches proposed suggested by Hendrik Tews to fix existential variables printing in emacs mode (put them at the end of input, and fix commas). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14818 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/printer.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) (limited to 'parsing') diff --git a/parsing/printer.ml b/parsing/printer.ml index 1c357076c..919ec188b 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -332,15 +332,16 @@ let emacs_print_dependent_evars sigma seeds = Intmap.fold begin fun e i s -> let e' = str (string_of_existential e) in match i with - | None -> s ++ e' ++ str " open," + | None -> s ++ str" " ++ e' ++ str " open," | Some i -> - s ++ e' ++ str " using " ++ + s ++ str " " ++ e' ++ str " using " ++ Intset.fold begin fun d s -> str (string_of_existential d) ++ str " " ++ s - end i (str "") + end i (str ",") end evars (str "") in - str "(dependent evars: " ++ evars ++ str ")" ++ fnl () + cut () ++ + str "(dependent evars:" ++ evars ++ str ")" ++ fnl () in delayed_emacs_cmd evars @@ -365,8 +366,8 @@ let default_pr_subgoals close_cmd sigma seeds = function | [g] -> let pg = default_pr_goal { it = g ; sigma = sigma } in v 0 ( - emacs_print_dependent_evars sigma seeds ++ str ("1 "^"subgoal") ++ pr_goal_tag g ++ cut () ++ pg + ++ emacs_print_dependent_evars sigma seeds ) | g1::rest -> let rec pr_rec n = function @@ -379,10 +380,10 @@ let default_pr_subgoals close_cmd sigma seeds = function let pg1 = default_pr_goal { it = g1 ; sigma = sigma } in let prest = pr_rec 2 rest in v 0 ( - emacs_print_dependent_evars sigma seeds ++ int(List.length rest+1) ++ str" subgoals" ++ str (emacs_str ", subgoal 1") ++ pr_goal_tag g1 ++ cut () ++ pg1 ++ prest ++ fnl () + ++ emacs_print_dependent_evars sigma seeds ) (**********************************************************************) -- cgit v1.2.3