diff options
| author | courtieu | 2011-05-24 19:01:42 +0000 |
|---|---|---|
| committer | courtieu | 2011-05-24 19:01:42 +0000 |
| commit | 77f1db2c35d3d337f4a47dc98d02f3c4749d9ade (patch) | |
| tree | a591fc7c1e0730f3489ff156a9b650a7da8d3d95 /parsing/printer.ml | |
| parent | 4b0102ef92f22b9f81a2b8fb3fa72a5c434f3cfe (diff) | |
Made the emacs-U option deprecated. Also removed the old code
inserting special chars for proof by pointing with emacs. This was
interacting badly with utf8. It may be implemented back with xml-like
tags instead of special chars.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14154 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/printer.ml')
| -rw-r--r-- | parsing/printer.ml | 15 |
1 files changed, 6 insertions, 9 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index 10ccd879ba..e99dc2b1c6 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -27,11 +27,8 @@ open Tacexpr open Store.Field -let emacs_str s alts = - match !Flags.print_emacs, !Flags.print_emacs_safechar with - | true, true -> alts - | true , false -> s - | false,_ -> "" +let emacs_str s = + if !Flags.print_emacs then s else "" (**********************************************************************) (** Terms *) @@ -220,7 +217,7 @@ let pr_context_limit n env = else let pidt = pr_var_decl env d in (i+1, (pps ++ fnl () ++ - str (emacs_str (String.make 1 (Char.chr 253)) "") ++ + str (emacs_str "") ++ pidt))) env ~init:(0,(mt ())) in @@ -229,7 +226,7 @@ let pr_context_limit n env = (fun env d pps -> let pnat = pr_rel_decl env d in (pps ++ fnl () ++ - str (emacs_str (String.make 1 (Char.chr 253)) "") ++ + str (emacs_str "") ++ pnat)) env ~init:(mt ()) in @@ -267,7 +264,7 @@ let default_pr_goal gs = in preamb ++ str" " ++ hv 0 (penv ++ fnl () ++ - str (emacs_str (String.make 1 (Char.chr 253)) "") ++ + str (emacs_str "") ++ str "============================" ++ fnl () ++ thesis ++ str " " ++ pc) ++ fnl () @@ -276,7 +273,7 @@ let pr_concl n sigma g = let (g,sigma) = Goal.V82.nf_evar sigma g in let env = Goal.V82.env sigma g in let pc = pr_ltype_env_at_top env (Goal.V82.concl sigma g) in - str (emacs_str (String.make 1 (Char.chr 253)) "") ++ + str (emacs_str "") ++ str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" " ++ pc (* display evar type: a context and a type *) |