]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/matitaWiki.ml
More statuses converted to objects.
[helm.git] / helm / software / matita / matitaWiki.ml
index 268da7e51c32142d3305100f27194f3b0576ac40..b52e75741f04b11fb25d9cc08b304aa420bc6cb0 100644 (file)
@@ -149,7 +149,7 @@ let rec interactive_loop () =
     | `Do command ->
         let str = Ulexing.from_utf8_string command in
         let watch_statuses grafite_status =
-         match grafite_status.GrafiteTypes.proof_status with
+         match grafite_status#proof_status with
             GrafiteTypes.Incomplete_proof
              {GrafiteTypes.proof = uri,metasenv,_subst,bo,ty,attrs ;
               GrafiteTypes.stack = stack } ->
@@ -225,7 +225,7 @@ let main () =
     let proof_status,moo_content_rev,lexicon_content_rev,dump = 
       match !grafite_status with
       |  s::_ ->
-         s.proof_status, s.moo_content_rev,
+         s#proof_status, s#moo_content_rev,
           (GrafiteTypes.get_estatus s)#lstatus.LexiconEngine.lexicon_content_rev,
           (GrafiteTypes.get_estatus s)#dump
       | _ -> assert false