many changes:

[helm.git] / components / lexicon / lexiconEngine.ml

diff --git a/components/lexicon/lexiconEngine.ml b/components/lexicon/lexiconEngine.ml
index 34e314edcd128b13ae820f1e393ea5df5801c49f..a0792d2281fd09bfc4ecf2fa0d05beb7ddf23327 100644 (file)
--- a/components/lexicon/lexiconEngine.ml
+++ b/components/lexicon/lexiconEngine.ml
@@ -25,7 +25,12 @@
 
 (* $Id$ *)
 
-exception IncludedFileNotCompiled of string (* file name *)
+let out = ref ignore
+
+let set_callback f = out := f
+
+(* lexicon file name * ma file name *)
+exception IncludedFileNotCompiled of string * string 
 exception MetadataNotFound of string        (* file name *)
 
 type status = {
@@ -111,11 +116,12 @@ let set_proof_aliases mode status new_aliases =
 
 
 let rec eval_command ?(mode=LexiconAst.WithPreferences) status cmd =
+ !out cmd;
  let notation_ids' = CicNotation.process_notation cmd in
  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 +131,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