Previous patch improved: we now use an ad-hoc wrapper for Grammar.parsable

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

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index 04cbb9a8fde4fa493015812b84701ef30390d256..b84180037b5ad92716267ce1022b19cc74e72550 100644 (file)
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -99,28 +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
-     (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 =
@@ -140,9 +118,14 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us
       let status = script#grafite_status in
       let _,_,menv,subst,_ = status#obj in
       let ctx = 
-        try let _,(_,ctx,_) = List.hd menv in ctx
-        with Failure "hd" -> []
-      in
+       match Continuationals.Stack.head_goals status#stack with
+          [] -> []
+        | g::tl ->
+           if tl <> [] then
+            HLog.warn
+             "Many goals focused. Using the context of the first one\n";
+           let _, ctx, _ = NCicUtils.lookup_meta g menv in
+            ctx in
       let m, s, status, t = 
         GrafiteDisambiguate.disambiguate_nterm 
           status None ctx menv subst (parsed_text,parsed_text_length,
@@ -210,12 +193,11 @@ 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 strm =
+         GrafiteParser.parsable_statement grafite_status
+          (Ulexing.from_utf8_string text) in
+        let ast = MatitaEngine.get_ast grafite_status include_paths strm in
+         ast, text
     | `Ast (st, text) -> st, text
   in
   let text_of_loc floc = 
@@ -683,9 +665,10 @@ object (self)
   method eos = 
     let rec is_there_only_comments lexicon_status s = 
       if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
-      match
-       GrafiteParser.parse_statement lexicon_status (Ulexing.from_utf8_string s)
-      with
+      let strm =
+       GrafiteParser.parsable_statement lexicon_status
+        (Ulexing.from_utf8_string s)in
+      match GrafiteParser.parse_statement lexicon_status strm with
       | GrafiteAst.Comment (loc,_) -> 
           let _,parsed_text_length = MatitaGtkMisc.utf8_parsed_text s loc in
           (* CSC: why +1 in the following lines ???? *)