X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaScript.ml;h=04cbb9a8fde4fa493015812b84701ef30390d256;hb=939dfce0cb12f7e7760a24d89f6812890b9df431;hp=9fc79ca9261245520309698de312b744b76b3e02;hpb=729e08f5fb86b3ffee460fda4577b024ab5888aa;p=helm.git

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index 9fc79ca92..04cbb9a8f 100644
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -67,7 +67,7 @@ let first_line s =
 
 type guistuff = {
   mathviewer:MatitaTypes.mathViewer;
-  urichooser: UriManager.uri list -> UriManager.uri list;
+  urichooser: NReference.reference list -> NReference.reference list;
   ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL];
 }
 
@@ -80,7 +80,7 @@ let eval_with_engine include_paths guistuff grafite_status user_goal
   let text = skipped_txt ^ nonskipped_txt in
   let prefix_len = MatitaGtkMisc.utf8_string_length skipped_txt in
   let enriched_history_fragment =
-   MatitaEngine.eval_ast ~do_heavy_checks:(Helm_registry.get_bool
+   MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:(Helm_registry.get_bool
      "matita.do_heavy_checks")
     grafite_status (text,prefix_len,st)
   in
@@ -92,7 +92,7 @@ let eval_with_engine include_paths guistuff grafite_status user_goal
        match alias with
        | None -> (status,to_prepend ^ nonskipped_txt)::acc,""
        | Some (k,value) ->
-            let newtxt = LexiconAstPp.pp_alias value in
+            let newtxt = GrafiteAstPp.pp_alias value in
             (status,to_prepend ^ newtxt ^ "\n")::acc, "")
       ([],skipped_txt) enriched_history_fragment
   in
@@ -103,11 +103,11 @@ let eval_with_engine include_paths guistuff grafite_status user_goal
  * so that we can ensure the inclusion is performed after the included file 
  * is compiled (if needed). matitac does not need that, since it compiles files
  * in the good order, here files may be compiled on demand. *)
-let wrap_with_make include_paths (f : #LexiconEngine.status GrafiteParser.statement) x = 
-  try      
-    f ~never_include:true ~include_paths x
-  with
-  | GrafiteParser.NoInclusionPerformed mafilename ->
+let wrap_with_make include_paths f x = 
+  match f x with
+     (GrafiteAst.Executable
+       (_,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,mafilename)))) as cmd
+     ->
       let root, buri, _, tgt = 
         try Librarian.baseuri_of_script ~include_paths mafilename
         with Librarian.NoRootFor _ -> 
@@ -115,18 +115,13 @@ let wrap_with_make include_paths (f : #LexiconEngine.status GrafiteParser.statem
           HLog.error "please create it.";
           raise (Failure ("No root file for "^mafilename))
       in
-      let b = MatitacLib.Make.make root [tgt] in
-      if b then 
-        try f ~include_paths x with LexiconEngine.IncludedFileNotCompiled _ ->
-         raise 
-           (Failure ("Including: "^tgt^
-             "\nNothing to do... did you run matitadep?"))
+      if MatitacLib.Make.make root [tgt] then
+       cmd
       else raise (Failure ("Compiling: " ^ tgt))
+   | cmd -> cmd
 ;;
 
-let pp_eager_statement_ast =
-  GrafiteAstPp.pp_statement ~term_pp:NotationPp.pp_term
-    ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false)
+let pp_eager_statement_ast = GrafiteAstPp.pp_statement 
 
 let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac =
   let parsed_text_length = String.length parsed_text in
@@ -150,7 +145,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us
       in
       let m, s, status, t = 
         GrafiteDisambiguate.disambiguate_nterm 
-          None status ctx menv subst (parsed_text,parsed_text_length,
+          status None ctx menv subst (parsed_text,parsed_text_length,
             NotationPt.Cast (t,NotationPt.Implicit `JustOne))  
           (* XXX use the metasenv, if possible *)
       in
@@ -211,17 +206,17 @@ script ex loc
 and eval_statement include_paths (buffer : GText.buffer) guistuff 
  grafite_status user_goal script statement
 =
-  let (grafite_status,st), unparsed_text =
+  let st,unparsed_text =
     match statement with
     | `Raw text ->
         if Pcre.pmatch ~rex:only_dust_RE text then raise Margin;
         let ast = 
          wrap_with_make include_paths
-          (GrafiteParser.parse_statement (Ulexing.from_utf8_string text)) 
-            grafite_status
+          (GrafiteParser.parse_statement grafite_status)
+            (Ulexing.from_utf8_string text)
         in
           ast, text
-    | `Ast (st, text) -> (grafite_status, st), text
+    | `Ast (st, text) -> st, text
   in
   let text_of_loc floc = 
     let nonskipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in
@@ -233,20 +228,16 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff
     txt,nonskipped_txt,skipped_txt,len
   in 
   match st with
-  | GrafiteParser.LNone loc ->
-      let parsed_text, _, _, parsed_text_length = text_of_loc loc in
-       [grafite_status,parsed_text],"",
-        parsed_text_length
-  | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) ->
+  | GrafiteAst.Executable (loc, ex) ->
      let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in
       eval_executable include_paths buffer guistuff 
        grafite_status user_goal unparsed_text skipped nonskipped script ex loc
-  | GrafiteParser.LSome (GrafiteAst.Comment (loc, GrafiteAst.Code (_, ex))) 
+  | GrafiteAst.Comment (loc, GrafiteAst.Code (_, ex))
     when Helm_registry.get_bool "matita.execcomments" ->
      let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in
       eval_executable include_paths buffer guistuff 
        grafite_status user_goal unparsed_text skipped nonskipped script ex loc
-  | GrafiteParser.LSome (GrafiteAst.Comment (loc, _)) -> 
+  | GrafiteAst.Comment (loc, _) -> 
       let parsed_text, _, _, parsed_text_length = text_of_loc loc in
       let remain_len = String.length unparsed_text - parsed_text_length in
       let s = String.sub unparsed_text parsed_text_length remain_len in
@@ -282,19 +273,16 @@ class script  ~(source_view: GSourceView2.source_view)
 let buffer = source_view#buffer in
 let source_buffer = source_view#source_buffer in
 let initial_statuses current baseuri =
- let empty_lstatus = new LexiconEngine.status in
+ let empty_lstatus = new GrafiteDisambiguate.status in
  (match current with
      Some current ->
-      LexiconSync.time_travel ~present:current ~past:empty_lstatus;
-      GrafiteSync.time_travel ~present:current ();
+      NCicLibrary.time_travel
+       ((new GrafiteTypes.status current#baseuri)#set_disambiguate_db current#disambiguate_db);
       (* CSC: there is a known bug in invalidation; temporary fix here *)
       NCicEnvironment.invalidate ()
    | None -> ());
- let lexicon_status =
-   CicNotation2.load_notation ~include_paths:[] empty_lstatus
-     BuildTimeConf.core_notation_script 
- in
- let grafite_status = GrafiteSync.init lexicon_status baseuri in
+ let lexicon_status = empty_lstatus in
+ let grafite_status = (new GrafiteTypes.status baseuri)#set_disambiguate_db lexicon_status#disambiguate_db in
   grafite_status
 in
 let read_include_paths file =
@@ -423,14 +411,8 @@ object (self)
       bottom) and we will face a macro *)
     userGoal <- None
 
-  method private _retract offset grafite_status new_statements
-   new_history
-  =
-   let cur_grafite_status =
-    match history with s::_ -> s | [] -> assert false
-   in
-    LexiconSync.time_travel ~present:cur_grafite_status ~past:grafite_status;
-    GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status ();
+  method private _retract offset grafite_status new_statements new_history =
+    NCicLibrary.time_travel grafite_status;
     statements <- new_statements;
     history <- new_history;
     self#moveMark (- offset)
@@ -701,24 +683,21 @@ object (self)
   method eos = 
     let rec is_there_only_comments lexicon_status s = 
       if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
-      let lexicon_status,st =
-       GrafiteParser.parse_statement (Ulexing.from_utf8_string s)
-        ~include_paths:self#include_paths lexicon_status
-      in
-      match st with
-      | GrafiteParser.LSome (GrafiteAst.Comment (loc,_)) -> 
+      match
+       GrafiteParser.parse_statement lexicon_status (Ulexing.from_utf8_string s)
+      with
+      | GrafiteAst.Comment (loc,_) -> 
           let _,parsed_text_length = MatitaGtkMisc.utf8_parsed_text s loc in
           (* CSC: why +1 in the following lines ???? *)
           let parsed_text_length = parsed_text_length + 1 in
           let remain_len = String.length s - parsed_text_length in
           let next = String.sub s parsed_text_length remain_len in
           is_there_only_comments lexicon_status next
-      | GrafiteParser.LNone _
-      | GrafiteParser.LSome (GrafiteAst.Executable _) -> false
+      | GrafiteAst.Executable _ -> false
     in
     try is_there_only_comments self#grafite_status self#getFuture
     with 
-    | LexiconEngine.IncludedFileNotCompiled _
+    | NCicLibrary.IncludedFileNotCompiled _
     | HExtlib.Localized _
     | CicNotationParser.Parse_error _ -> false
     | Margin | End_of_file -> true