big change in parsing, trying to make all functional

[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 8eb438e185866d44507e65fbc12496650ff80d9c..00160ac81b0ad885d47fe7477ce5f94f3a3f93c5 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -554,7 +554,18 @@ let eval_comment opts status (text,prefix_len,c) = status, []
 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