X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitacLib.ml;h=6d01fc460f665ca861d71a96c120d881d648af4d;hb=73a66cce6e72c654fdcd0ce760c405a74af70d08;hp=b3b95325acc8a66ec7fc7e6c5237538975fb7078;hpb=df1201e37d6f2631dc31ffc87b979a6c81180a3a;p=helm.git

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index b3b95325a..6d01fc460 100644
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -29,7 +29,7 @@ open Printf
 
 open GrafiteTypes
 
-exception AttemptToInsertAnAlias of #LexiconEngine.status
+exception AttemptToInsertAnAlias of LexiconEngine.status
 
 let slash_n_RE = Pcre.regexp "\\n" ;;
 
@@ -69,7 +69,7 @@ let dump f =
    let och = open_out f in
    let nl () =  output_string och (pp_statement nl_ast) in
    MatitaMisc.out_preamble och;
-   let grafite_parser_cb status = function
+   let grafite_parser_cb = function
       | G.Executable (_, G.Macro (_, G.Inline (_, uri, params))) ->
          let str =
             ApplyTransformation.txt_of_inline_macro params uri
@@ -77,11 +77,11 @@ let dump f =
 	          (Helm_registry.get_bool "matita.paste_unicode_as_tex")
 	 in
          output_string och str
-      | G.Executable (loc, G.Command (_, G.Include (_, false, _))) -> ()
+      | G.Executable (loc, G.Command (_, G.Include (_, false, _, _))) -> ()
       | stm ->
          output_string och (pp_statement stm); nl (); nl ()
    in
-   let lexicon_parser_cb status cmd =
+   let lexicon_parser_cb cmd =
          output_string och (pp_lexicon cmd); nl (); nl ()
    in
    begin fun () ->
@@ -91,15 +91,15 @@ let dump f =
    end, 
    begin fun x ->
       close_out och;
-      GrafiteParser.set_grafite_callback (fun _ _ -> ());
-      GrafiteParser.set_lexicon_callback (fun _ _ -> ());
+      GrafiteParser.set_grafite_callback (fun _ -> ());
+      GrafiteParser.set_lexicon_callback (fun _ -> ());
       Helm_registry.set_bool "matita.moo" true;
       x
    end
 ;;
 
 let get_macro_context = function
-   | Some {GrafiteTypes.proof_status = GrafiteTypes.No_proof} -> []
+   | Some status when status#proof_status = GrafiteTypes.No_proof -> []
    | Some status                ->
       let stack = GrafiteTypes.get_stack status in
       let goal = Continuationals.Stack.find_goal stack in
@@ -235,8 +235,8 @@ let compile atstart options fname =
       with
       | [] -> grafite_status
       | (g,None)::_ -> g
-      | (g,Some _)::_ -> 
-            raise (AttemptToInsertAnAlias (GrafiteTypes.get_estatus g))
+      | (g,Some _)::_ ->
+         raise (AttemptToInsertAnAlias (g :> LexiconEngine.status))
      with MatitaEngine.EnrichedWithStatus 
             (GrafiteEngine.Macro (floc, f), grafite) as exn ->
             match f (get_macro_context (Some grafite)) with 
@@ -257,8 +257,8 @@ let compile atstart options fname =
     in
     let elapsed = Unix.time () -. time in
     let proof_status,moo_content_rev,lexicon_content_rev = 
-      grafite_status.proof_status, grafite_status.moo_content_rev, 
-       (GrafiteTypes.get_estatus grafite_status)#lstatus.LexiconEngine.lexicon_content_rev
+      grafite_status#proof_status, grafite_status#moo_content_rev, 
+       grafite_status#lstatus.LexiconEngine.lexicon_content_rev
     in
     if proof_status <> GrafiteTypes.No_proof then
      (HLog.error
@@ -275,7 +275,7 @@ let compile atstart options fname =
         GrafiteMarshal.save_moo moo_fname moo_content_rev;
         LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
         NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
-         (GrafiteTypes.get_estatus grafite_status)#dump
+         grafite_status#dump
      end;
      let tm = Unix.gmtime elapsed in
      let sec = string_of_int tm.Unix.tm_sec ^ "''" in