merged cic_notation with matita: good luck!

[helm.git] / helm / matita / matitaScript.ml

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 4a6115813e708ecbaf57c6394a155a5c62fd142d..f1a0e6429622490e4973fd1aa218ff284e33a3cc 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -61,8 +61,8 @@ let prepend_text header base =
 
   (** creates a statement AST for the Goal tactic, e.g. "goal 7" *)
 let goal_ast n =
-  let module A = TacticAst in
-  let loc = CicAst.dummy_floc in
+  let module A = GrafiteAst in
+  let loc = Disambiguate.dummy_floc in
   A.Executable (loc, A.Tactical (loc, A.Tactic (loc, A.Goal (loc, n))))
 
 type guistuff = {
@@ -74,8 +74,8 @@ type guistuff = {
 }
 
 let eval_with_engine guistuff status user_goal parsed_text st =
-  let module TA = TacticAst in
-  let module TAPp = TacticAstPp in
+  let module TA = GrafiteAst in
+  let module TAPp = GrafiteAstPp in
   let include_ = 
     match guistuff.filenamedata with
     | None,None -> []
@@ -130,7 +130,7 @@ let eval_with_engine guistuff status user_goal parsed_text st =
     if DisambiguateTypes.Environment.is_empty new_aliases then
       parsed_text
     else
-      prepend_text (CicTextualParser2.EnvironmentP3.to_string new_aliases)
+      prepend_text (DisambiguatePp.pp_environment new_aliases)
         parsed_text
   in
   let new_text =
@@ -208,8 +208,8 @@ let disambiguate term status =
  
 let eval_macro guistuff status parsed_text script mac
 =
-  let module TA = TacticAst in
-  let module TAPp = TacticAstPp in
+  let module TA = GrafiteAst in
+  let module TAPp = GrafiteAstPp in
   let module MQ = MetadataQuery in
   let module MDB = MatitaDb in
   let module CTC = CicTypeChecker in
@@ -267,7 +267,7 @@ let eval_macro guistuff status parsed_text script mac
          TA.Executable (loc,
           (TA.Tactical (loc, 
             TA.Tactic (loc,
-             TA.Apply (loc, CicAst.Uri (UriManager.string_of_uri uri,None))))))
+             TA.Apply (loc, CicNotationPt.Uri (UriManager.string_of_uri uri,None))))))
         in
         let new_status = MatitaEngine.eval_ast status ast in
         let extra_text = 
@@ -323,8 +323,8 @@ let eval_macro guistuff status parsed_text script mac
 
                                 
 let eval_executable guistuff status user_goal parsed_text script ex =
-  let module TA = TacticAst in
-  let module TAPp = TacticAstPp in
+  let module TA = GrafiteAst in
+  let module TAPp = GrafiteAstPp in
   let module MD = MatitaDisambiguator in
   let module ML = MatitacleanLib in
   let parsed_text_length = String.length parsed_text in
@@ -354,14 +354,14 @@ let eval_executable guistuff status user_goal parsed_text script ex =
 
 let rec eval_statement guistuff status user_goal script s =
   if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
-  let st = CicTextualParser2.parse_statement (Stream.of_string s) in
+  let st = GrafiteParser.parse_statement (Stream.of_string s) in
   let text_of_loc loc =
-    let parsed_text_length = snd (CicAst.loc_of_floc loc) in
+    let parsed_text_length = snd (CicNotationPt.loc_of_floc loc) in
     let parsed_text = safe_substring s 0 parsed_text_length in
     parsed_text, parsed_text_length
   in
   match st with
-  | TacticAst.Comment (loc,_)-> 
+  | GrafiteAst.Comment (loc,_)-> 
       let parsed_text, parsed_text_length = text_of_loc loc in
       let remain_len = String.length s - parsed_text_length in
       let s = String.sub s parsed_text_length remain_len in
@@ -372,7 +372,7 @@ let rec eval_statement guistuff status user_goal script s =
       | (status, text) :: tl ->
         ((status, parsed_text ^ text)::tl), (parsed_text_length + len)
       | [] -> [], 0)
-  | TacticAst.Executable (loc, ex) ->
+  | GrafiteAst.Executable (loc, ex) ->
       let parsed_text, parsed_text_length = text_of_loc loc in
       eval_executable guistuff  status user_goal parsed_text script ex 
   
@@ -638,19 +638,19 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
     let s = self#getFuture in
     let rec is_there_and_executable s = 
       if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
-      let st = CicTextualParser2.parse_statement (Stream.of_string s) in
+      let st = GrafiteParser.parse_statement (Stream.of_string s) in
       match st with
-      | TacticAst.Comment (loc,_)-> 
-          let parsed_text_length = snd (CicAst.loc_of_floc loc) in
+      | GrafiteAst.Comment (loc,_)-> 
+          let parsed_text_length = snd (CicNotationPt.loc_of_floc loc) in
           let remain_len = String.length s - parsed_text_length in
           let next = String.sub s parsed_text_length remain_len in
           is_there_and_executable next
-      | TacticAst.Executable (loc, ex) -> false
+      | GrafiteAst.Executable (loc, ex) -> false
     in
     try
       is_there_and_executable s
     with 
-    | CicTextualParser2.Parse_error _ -> false
+    | CicNotationParser.Parse_error _ -> false
     | Margin -> true