X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaScript.ml;h=6aae0020da0d3a0a6b2091b46f179dac8ea40890;hb=f167565ea9faf28f4e3d76b8f160fd269cd1aa84;hp=b8a72a4d24e53dc0fc190ec388d6fc17c11e9141;hpb=30bbfa78612ca1ad0c131a75d7075cfd35bebbe1;p=helm.git

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index b8a72a4d2..6aae0020d 100644
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -99,27 +99,6 @@ let eval_with_engine include_paths guistuff grafite_status user_goal
   res,"",parsed_text_length
 ;;
 
-(* this function calls the parser in a way that it does not perform inclusions,
- * 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 x = 
-  match f x with
-     GrafiteParser.LSome (GrafiteAst.Executable (_,GrafiteAst.NCommand
-     (_,GrafiteAst.Include (_,_,mafilename)))) as cmd ->
-      let root, buri, _, tgt = 
-        try Librarian.baseuri_of_script ~include_paths mafilename
-        with Librarian.NoRootFor _ -> 
-          HLog.error ("The included file '"^mafilename^"' has no root file,");
-          HLog.error "please create it.";
-          raise (Failure ("No root file for "^mafilename))
-      in
-      if MatitacLib.Make.make root [tgt] then
-       cmd
-      else raise (Failure ("Compiling: " ^ tgt))
-   | cmd -> cmd
-;;
-
 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 =
@@ -144,7 +123,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
@@ -209,12 +188,8 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff
     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 grafite_status)
-            (Ulexing.from_utf8_string text)
-        in
-          ast, text
+        let ast = MatitaEngine.toplevel grafite_status include_paths text in
+         ast, text
     | `Ast (st, text) -> st, text
   in
   let text_of_loc floc = 
@@ -227,20 +202,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
@@ -276,16 +247,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 LexiconTypes.status in
+ let empty_lstatus = new GrafiteDisambiguate.status in
  (match current with
      Some current ->
       NCicLibrary.time_travel
-       ((new GrafiteTypes.status current#baseuri)#set_lstatus current#lstatus);
+       ((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 = empty_lstatus in
- let grafite_status = (new GrafiteTypes.status baseuri)#set_lstatus lexicon_status#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 =
@@ -689,15 +660,14 @@ object (self)
       match
        GrafiteParser.parse_statement lexicon_status (Ulexing.from_utf8_string s)
       with
-      | GrafiteParser.LSome (GrafiteAst.Comment (loc,_)) -> 
+      | 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