Remplacement Pp.qs par Pptactic.qsnew

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7751 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 28 insertions, 44 deletions

diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 4609d4b2e..8476ccf2a 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -296,20 +296,6 @@ let strip_prod_binders_expr n ty =
       | _ -> error "Cannot translate fix tactic: not enough products" in
   strip_ty [] n ty
 
-
-(* In new syntax only double quote char is escaped by repeating it *)
-let rec escape_string s =
-  let rec escape_at s i =
-    if i<0 then s
-    else if s.[i] == '"' then
-      let s' = String.sub s 0 i^"\""^String.sub s i (String.length s - i) in
-      escape_at s' (i-1)
-    else escape_at s (i-1) in
-  escape_at s (String.length s - 1)
-
-let qstring s = str ("\""^escape_string s^"\"")
-let qsnew = qstring
-
 let pr_ltac_or_var pr = function
   | ArgArg x -> pr x
   | ArgVar (loc,id) -> pr_with_comments loc (pr_id id)
@@ -863,13 +849,13 @@ let rec pr_tac env inherited tac =
   | TacFail (ArgArg 0,"") -> str "fail", latom
   | TacFail (n,s) -> 
       str "fail" ++ (if n=ArgArg 0 then mt () else pr_arg (pr_or_var int) n) ++
-      (if s="" then mt() else (spc() ++ qstring s)), latom
+      (if s="" then mt() else (spc() ++ qs s)), latom
   | TacFirst tl ->
       str "first" ++ spc () ++ pr_seq_body (pr_tac env ltop) tl, llet
   | TacSolve tl ->
       str "solve" ++ spc () ++ pr_seq_body (pr_tac env ltop) tl, llet
   | TacId "" -> str "idtac", latom
-  | TacId s -> str "idtac" ++ (qstring s), latom
+  | TacId s -> str "idtac" ++ (qs s), latom
   | TacAtom (loc,TacAlias (_,s,l,_)) ->
       pr_with_comments loc
         (pr_extend env (level_of inherited) s (List.map snd l)),
@@ -881,7 +867,7 @@ let rec pr_tac env inherited tac =
       str "constr:" ++ pr_constr env c, latom
   | TacArg(ConstrMayEval c) ->
       pr_may_eval (pr_constr env) (pr_lconstr env) (pr_cst env) c, leval
-  | TacArg(TacFreshId sopt) -> str "fresh" ++ pr_opt qstring sopt, latom
+  | TacArg(TacFreshId sopt) -> str "fresh" ++ pr_opt qs sopt, latom
   | TacArg(Integer n) -> int n, latom
   | TacArg(TacCall(loc,f,l)) ->
       pr_with_comments loc
@@ -902,9 +888,9 @@ and pr_tacarg env = function
   | Reference r -> pr_ref r
   | ConstrMayEval c ->
       pr_may_eval (pr_constr env) (pr_lconstr env) (pr_cst env) c
-  | TacFreshId sopt -> str "fresh" ++ pr_opt qstring sopt
+  | TacFreshId sopt -> str "fresh" ++ pr_opt qs sopt
   | TacExternal (_,com,req,la) ->
-      str "external" ++ spc() ++ qstring com ++ spc() ++ qstring req ++ 
+      str "external" ++ spc() ++ qs com ++ spc() ++ qs req ++ 
       spc() ++ prlist_with_sep spc (pr_tacarg env) la
   | (TacCall _|Tacexp _|Integer _) as a ->
       str "ltac:" ++ pr_tac env (latom,E) (TacArg a)
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index 60c41736b..05faff2cd 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -77,8 +77,6 @@ val pr_extend :
   (tolerability -> glob_tactic_expr -> std_ppcmds) -> int ->
     string -> closed_generic_argument list -> std_ppcmds
 
-val qsnew : string -> std_ppcmds
-
 val pr_intro_pattern : intro_pattern_expr -> std_ppcmds
 
 val pr_raw_tactic : env -> raw_tactic_expr -> std_ppcmds
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index f7782d6d5..41c391802 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -121,11 +121,11 @@ let strip_meta id =
 let pr_production_item = function
   | VNonTerm (loc,nt,Some p) -> str nt ++ str"(" ++ pr_id (strip_meta p) ++ str")"
   | VNonTerm (loc,nt,None) -> str nt
-  | VTerm s -> qsnew s
+  | VTerm s -> qs s
 
 let pr_comment pr_c = function
   | CommentConstr c -> pr_c c
-  | CommentString s -> qsnew s
+  | CommentString s -> qs s
   | CommentInt n -> int n
 
 let pr_in_out_modules = function
@@ -135,7 +135,7 @@ let pr_in_out_modules = function
 
 let pr_search_about = function
   | SearchRef r -> pr_reference r
-  | SearchString s -> qsnew s
+  | SearchString s -> qs s
 
 let pr_search a b pr_p = match a with
   | SearchHead qid -> str"Search" ++ spc() ++ pr_reference qid ++ pr_in_out_modules b
@@ -156,7 +156,7 @@ let pr_class_rawexpr = function
 
 let pr_option_ref_value = function
   | QualidRefValue id -> pr_reference id
-  | StringRefValue s -> qsnew s
+  | StringRefValue s -> qs s
 
 let pr_printoption a b = match a with
   | Goptions.PrimaryTable table -> str table ++ pr_opt (prlist_with_sep sep pr_option_ref_value) b
@@ -265,7 +265,7 @@ let pr_type_option pr_c = function
 
 let pr_decl_notation prc =
   pr_opt (fun (ntn,c,scopt) -> fnl () ++
-    str "where " ++ qsnew ntn ++ str " := " ++ prc c ++
+    str "where " ++ qs ntn ++ str " := " ++ prc c ++
     pr_opt (fun sc -> str ": " ++ str sc) scopt)
 
 let pr_vbinders l =
@@ -346,7 +346,7 @@ let pr_syntax_modifier = function
   | SetAssoc Gramext.NonA -> str"no associativity"
   | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ
   | SetOnlyParsing -> str"only parsing"
-  | SetFormat s -> str"format " ++ pr_located qsnew s
+  | SetFormat s -> str"format " ++ pr_located qs s
 
 let pr_syntax_modifiers = function
   | [] -> mt()
@@ -372,8 +372,8 @@ in str"<" ++ pr_boxkind b ++ str">"
 let pr_paren_reln_or_extern = function
   | None,L -> str"L"
   | None,E -> str"E"
-  | Some pprim,Any -> qsnew pprim
-  | Some pprim,Prec p -> qsnew pprim ++ spc() ++ str":" ++ spc() ++ int p
+  | Some pprim,Any -> qs pprim
+  | Some pprim,Prec p -> qs pprim ++ spc() ++ str":" ++ spc() ++ int p
   | _ -> mt()
 
 (**************************************)
@@ -431,8 +431,8 @@ let rec pr_vernac = function
   | VernacBackTo i -> str"BackTo" ++ pr_intarg i
 
   (* State management *)
-  | VernacWriteState s -> str"Write State" ++ spc () ++ qsnew s
-  | VernacRestoreState s -> str"Restore State" ++ spc() ++ qsnew s
+  | VernacWriteState s -> str"Write State" ++ spc () ++ qs s
+  | VernacRestoreState s -> str"Restore State" ++ spc() ++ qs s
 
   (* Control *)
   | VernacList l ->
@@ -440,7 +440,7 @@ let rec pr_vernac = function
              prlist (fun v -> pr_located pr_vernac v ++ sep_end () ++ fnl()) l
              ++ spc() ++ str"]") 
   | VernacLoad (f,s) -> str"Load" ++ if f then (spc() ++ str"Verbose"
-  ++ spc()) else spc()  ++ qsnew s
+  ++ spc()) else spc()  ++ qs s
   | VernacTime v -> str"Time" ++ spc() ++ pr_vernac v
   | VernacVar id -> pr_lident id
   
@@ -461,7 +461,7 @@ let rec pr_vernac = function
     str"Arguments Scope" ++ spc() ++ pr_reference q ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]"
   | VernacInfix (local,(s,mv),q,sn) -> (* A Verifier *)
       hov 0 (hov 0 (str"Infix " ++ pr_locality local
-      ++ qsnew s ++ str " :=" ++ spc() ++ pr_reference q) ++
+      ++ qs s ++ str " :=" ++ spc() ++ pr_reference q) ++
       pr_syntax_modifiers mv ++
       (match sn with
     | None -> mt()
@@ -472,15 +472,15 @@ let rec pr_vernac = function
 	if n > 2 & s.[0] = '\'' & s.[n-1] = '\'' 
 	then
           let s' = String.sub s 1 (n-2) in
-          if String.contains s' '\'' then qsnew s else str s'
-	else qsnew s in
+          if String.contains s' '\'' then qs s else str s'
+	else qs s in
       hov 2( str"Notation" ++ spc() ++ pr_locality local ++ ps ++
       str " :=" ++ pr_constrarg c ++ pr_syntax_modifiers l ++
       (match opt with
         | None -> mt()
         | Some sc -> str" :" ++ spc() ++ str sc))
   | VernacSyntaxExtension (local,(s,l)) ->
-      str"Reserved Notation" ++ spc() ++ pr_locality local ++ qsnew s ++
+      str"Reserved Notation" ++ spc() ++ pr_locality local ++ qs s ++
       pr_syntax_modifiers l
 
   (* Gallina *)
@@ -694,20 +694,20 @@ let rec pr_vernac = function
         | None -> mt()
         | Some false -> str"Implementation" ++ spc()
         | Some true -> str"Specification" ++ spc ()) ++
-      qsnew f)
+      qs f)
   | VernacAddLoadPath (fl,s,d) -> hov 2
       (str"Add" ++
        (if fl then str" Rec " else spc()) ++
-       str"LoadPath" ++ spc() ++ qsnew s ++
+       str"LoadPath" ++ spc() ++ qs s ++
        (match d with 
          | None -> mt()
          | Some dir -> spc() ++ str"as" ++ spc() ++ pr_dirpath dir)) 
-  | VernacRemoveLoadPath s -> str"Remove LoadPath" ++ qsnew s
+  | VernacRemoveLoadPath s -> str"Remove LoadPath" ++ qs s
   | VernacAddMLPath (fl,s) ->
-      str"Add" ++ (if fl then str" Rec " else spc()) ++ str"ML Path" ++ qsnew s
+      str"Add" ++ (if fl then str" Rec " else spc()) ++ str"ML Path" ++ qs s
   | VernacDeclareMLModule l ->
-      hov 2 (str"Declare ML Module" ++ spc() ++ prlist_with_sep sep qsnew l)
-  | VernacChdir s -> str"Cd" ++ pr_opt qsnew s
+      hov 2 (str"Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l)
+  | VernacChdir s -> str"Cd" ++ pr_opt qs s
 
   (* Commands *)
   | VernacDeclareTacticDefinition (rc,l) ->
@@ -812,10 +812,10 @@ let rec pr_vernac = function
   | VernacLocate loc -> 
       let pr_locate =function
 	| LocateTerm qid ->  pr_reference qid
-	| LocateFile f -> str"File" ++ spc() ++ qsnew f
+	| LocateFile f -> str"File" ++ spc() ++ qs f
 	| LocateLibrary qid -> str"Library" ++ spc () ++ pr_module qid
 	| LocateModule qid -> str"Module" ++ spc () ++ pr_module qid
-	| LocateNotation s -> qsnew s
+	| LocateNotation s -> qs s
       in str"Locate" ++ spc() ++ pr_locate loc
   | VernacComments l ->
       hov 2