- the connections between the intermediate language and the "bag"

[helm.git] / matita / components / grafite_engine / grafiteEngine.ml

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index b12da380280b8219ad0ed0518b48b315154a4738..00160ac81b0ad885d47fe7477ce5f94f3a3f93c5 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -549,14 +549,23 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
       eval_add_constraint status [`Type,u1] [`Type,u2]
 ;;
 
-let eval_comment ~disambiguate_command opts status (text,prefix_len,c) =
- status, []
+let eval_comment opts status (text,prefix_len,c) = status, []
 
-let rec eval_command ~disambiguate_command opts status (text,prefix_len,cmd) =
- let status,cmd = disambiguate_command status (text,prefix_len,cmd) in
+let rec eval_command opts status (text,prefix_len,cmd) =
  let status,uris =
   match cmd with
-  | GrafiteAst.Include (loc, baseuri) ->
+  | GrafiteAst.Include (loc, fname, mode, _) ->
+                  let include_paths = assert false in
+                  let never_include = assert false in
+                  let mode = assert false in
+                  let baseuri = assert false in
+      let status =
+       let _root, buri, fullpath, _rrelpath = 
+          Librarian.baseuri_of_script ~include_paths fname in
+        if never_include then raise (GrafiteParser.NoInclusionPerformed fullpath) 
+        else
+           LexiconEngine.eval_command status (LexiconAst.Include (loc,buri,mode,fullpath)) 
+      in
      let status,obj =
        GrafiteTypes.Serializer.require ~baseuri:(NUri.uri_of_string baseuri)
         status in
@@ -567,7 +576,7 @@ let rec eval_command ~disambiguate_command opts status (text,prefix_len,cmd) =
  in
   status,uris
 
-and eval_executable ~disambiguate_command opts status (text,prefix_len,ex) =
+and eval_executable opts status (text,prefix_len,ex) =
   match ex with
   | GrafiteAst.NTactic (_(*loc*), tacl) ->
       if status#ng_mode <> `ProofMode then
@@ -582,19 +591,17 @@ and eval_executable ~disambiguate_command opts status (text,prefix_len,ex) =
        in
         status,[]
   | GrafiteAst.Command (_, cmd) ->
-      eval_command ~disambiguate_command opts status (text,prefix_len,cmd)
+      eval_command opts status (text,prefix_len,cmd)
   | GrafiteAst.NCommand (_, cmd) ->
       eval_ncommand opts status (text,prefix_len,cmd)
   | GrafiteAst.NMacro (loc, macro) ->
      raise (NMacro (loc,macro))
 
-and eval_ast ~disambiguate_command ?(do_heavy_checks=false) status
-(text,prefix_len,st)
-=
+and eval_ast ?(do_heavy_checks=false) status (text,prefix_len,st) =
   let opts = { do_heavy_checks = do_heavy_checks ; } in
   match st with
   | GrafiteAst.Executable (_,ex) ->
-     eval_executable ~disambiguate_command opts status (text,prefix_len,ex)
+     eval_executable opts status (text,prefix_len,ex)
   | GrafiteAst.Comment (_,c) -> 
-      eval_comment ~disambiguate_command opts status (text,prefix_len,c) 
+      eval_comment opts status (text,prefix_len,c) 
 ;;