]> matita.cs.unibo.it Git - helm.git/blobdiff - components/lexicon/lexiconEngine.ml
moved graphviz pretty printer outside matita, so that it can be used by other compone...
[helm.git] / components / lexicon / lexiconEngine.ml
index 34e314edcd128b13ae820f1e393ea5df5801c49f..1e1fe61c05147eef1dd8df67231df4f18ee3b7b1 100644 (file)
@@ -25,7 +25,8 @@
 
 (* $Id$ *)
 
-exception IncludedFileNotCompiled of string (* file name *)
+(* lexicon file name * ma file name *)
+exception IncludedFileNotCompiled of string * string 
 exception MetadataNotFound of string        (* file name *)
 
 type status = {
@@ -115,7 +116,7 @@ let rec eval_command ?(mode=LexiconAst.WithPreferences) status cmd =
  let status =
    { status with notation_ids = notation_ids' @ status.notation_ids } in
   match cmd with
-  | LexiconAst.Include (loc, baseuri, mode) ->
+  | LexiconAst.Include (loc, baseuri, mode, fullpath) ->
      let lexiconpath_rw, lexiconpath_r = 
        LibraryMisc.lexicon_file_of_baseuri 
          ~must_exist:false ~writable:true ~baseuri,
@@ -125,7 +126,7 @@ let rec eval_command ?(mode=LexiconAst.WithPreferences) status cmd =
      let lexiconpath = 
        if Sys.file_exists lexiconpath_rw then lexiconpath_rw else
          if Sys.file_exists lexiconpath_r then lexiconpath_r else
-          raise (IncludedFileNotCompiled lexiconpath_rw)
+          raise (IncludedFileNotCompiled (lexiconpath_rw,fullpath))
      in
      let lexicon = LexiconMarshal.load_lexicon lexiconpath in
      let status = List.fold_left (eval_command ~mode) status lexicon in