WARNING: partial commit.

- matita is compiling again, but totally untested
- major re-organization of the statuses

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index b12da380280b8219ad0ed0518b48b315154a4738..8eb438e185866d44507e65fbc12496650ff80d9c 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -549,11 +549,9 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
       eval_add_constraint status [`Type,u1] [`Type,u2]
 ;;
 
-let eval_comment ~disambiguate_command opts status (text,prefix_len,c) =
- status, []
+let eval_comment opts status (text,prefix_len,c) = status, []
 
-let rec eval_command ~disambiguate_command opts status (text,prefix_len,cmd) =
- let status,cmd = disambiguate_command status (text,prefix_len,cmd) in
+let rec eval_command opts status (text,prefix_len,cmd) =
  let status,uris =
   match cmd with
   | GrafiteAst.Include (loc, baseuri) ->
@@ -567,7 +565,7 @@ let rec eval_command ~disambiguate_command opts status (text,prefix_len,cmd) =
  in
   status,uris
 
-and eval_executable ~disambiguate_command opts status (text,prefix_len,ex) =
+and eval_executable opts status (text,prefix_len,ex) =
   match ex with
   | GrafiteAst.NTactic (_(*loc*), tacl) ->
       if status#ng_mode <> `ProofMode then
@@ -582,19 +580,17 @@ and eval_executable ~disambiguate_command opts status (text,prefix_len,ex) =
        in
         status,[]
   | GrafiteAst.Command (_, cmd) ->
-      eval_command ~disambiguate_command opts status (text,prefix_len,cmd)
+      eval_command opts status (text,prefix_len,cmd)
   | GrafiteAst.NCommand (_, cmd) ->
       eval_ncommand opts status (text,prefix_len,cmd)
   | GrafiteAst.NMacro (loc, macro) ->
      raise (NMacro (loc,macro))
 
-and eval_ast ~disambiguate_command ?(do_heavy_checks=false) status
-(text,prefix_len,st)
-=
+and eval_ast ?(do_heavy_checks=false) status (text,prefix_len,st) =
   let opts = { do_heavy_checks = do_heavy_checks ; } in
   match st with
   | GrafiteAst.Executable (_,ex) ->
-     eval_executable ~disambiguate_command opts status (text,prefix_len,ex)
+     eval_executable opts status (text,prefix_len,ex)
   | GrafiteAst.Comment (_,c) -> 
-      eval_comment ~disambiguate_command opts status (text,prefix_len,c) 
+      eval_comment opts status (text,prefix_len,c) 
 ;;

diff --git a/matita/components/grafite_engine/grafiteEngine.mli b/matita/components/grafite_engine/grafiteEngine.mli
index ad88d5dfd11909e07d40ddeedea3462902537ea8..10bc4d36de963cdc45c5397c21d51afa89ccdd71 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.mli
+++ b/matita/components/grafite_engine/grafiteEngine.mli
@@ -29,11 +29,6 @@ exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro
 type 'a disambiguator_input = string * int * 'a
 
 val eval_ast :
-  disambiguate_command:
-   (GrafiteTypes.status ->
-    GrafiteAst.command disambiguator_input ->
-    GrafiteTypes.status * GrafiteAst.command) ->
-
   ?do_heavy_checks:bool ->
   GrafiteTypes.status ->
   GrafiteAst.statement disambiguator_input ->

diff --git a/matita/components/grafite_engine/grafiteTypes.ml b/matita/components/grafite_engine/grafiteTypes.ml
index d36998181c887df94a11553341768bc219e04814..82fc6d605a97ba56c0d54167eb45468d01e45569 100644 (file)
--- a/matita/components/grafite_engine/grafiteTypes.ml
+++ b/matita/components/grafite_engine/grafiteTypes.ml
@@ -40,6 +40,7 @@ class status = fun (b : string) ->
    (* Warning: #stack and #obj are meaningful iff #ng_mode is `ProofMode *)
    inherit ([Continuationals.Stack.t] NTacStatus.status fake_obj (Continuationals.Stack.empty))
    inherit NCicLibrary.dumpable_status
+   inherit NCicLibrary.status
    val baseuri = b
    val ng_mode = (`CommandMode : [`CommandMode | `ProofMode])
    method baseuri = baseuri

diff --git a/matita/components/grafite_engine/grafiteTypes.mli b/matita/components/grafite_engine/grafiteTypes.mli
index f407cc49ba966843dee850f0031a20b92f198bcc..92af84babd4d0aecd2a6b5eae5a9f12b82a15044 100644 (file)
--- a/matita/components/grafite_engine/grafiteTypes.mli
+++ b/matita/components/grafite_engine/grafiteTypes.mli
@@ -37,6 +37,7 @@ class status :
    (* Warning: #stack and #obj are meaningful iff #ng_mode is `ProofMode *)
    inherit NTacStatus.tac_status
    inherit NCicLibrary.dumpable_status
+   inherit NCicLibrary.status
    method baseuri: string
    method set_baseuri: string -> 'self
    method ng_mode: [`ProofMode | `CommandMode]

diff --git a/matita/components/grafite_engine/nCicCoercDeclaration.ml b/matita/components/grafite_engine/nCicCoercDeclaration.ml
index 8ba2f92f88d5c1b2d60fe70771fbc2a80d010650..ca56a3aee4b38a7e2a2a8621980fa589b4e3540e 100644 (file)
--- a/matita/components/grafite_engine/nCicCoercDeclaration.ml
+++ b/matita/components/grafite_engine/nCicCoercDeclaration.ml
@@ -311,8 +311,7 @@ let basic_eval_and_record_ncoercion_from_t_cpos_arity
    status,uris
 ;;
 
-let eval_ncoercion status name t ty (id,src) tgt = 
-
+let eval_ncoercion (status: #GrafiteTypes.status) name t ty (id,src) tgt = 
  let metasenv,subst,status,ty =
   GrafiteDisambiguate.disambiguate_nterm None status [] [] [] ("",0,ty) in
  assert (metasenv=[]);
@@ -321,7 +320,6 @@ let eval_ncoercion status name t ty (id,src) tgt =
   GrafiteDisambiguate.disambiguate_nterm (Some ty) status [] [] [] ("",0,t) in
  assert (metasenv=[]);
  let t = NCicUntrusted.apply_subst subst [] t in
-
  let status, src, tgt, cpos, arity = 
    src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt in
  let status, uris =

diff --git a/matita/components/grafite_parser/grafiteDisambiguate.ml b/matita/components/grafite_parser/grafiteDisambiguate.ml
index f12a973721475eb5d9a3c261e6001a3b6f8fc0f8..143ac5e11f83949682d513dfd51bb0f39328f4c1 100644 (file)
--- a/matita/components/grafite_parser/grafiteDisambiguate.ml
+++ b/matita/components/grafite_parser/grafiteDisambiguate.ml
@@ -25,7 +25,7 @@
 
 (* $Id$ *)
 
-class g_status =
+class type g_status =
   object
    inherit LexiconEngine.g_status
    inherit NCicCoercion.g_status

diff --git a/matita/components/grafite_parser/grafiteDisambiguate.mli b/matita/components/grafite_parser/grafiteDisambiguate.mli
index 97ff558745c23f75ffe3af2139e59a609db48def..200d507a89d57db270a18ea3b920b08b842e8cb1 100644 (file)
--- a/matita/components/grafite_parser/grafiteDisambiguate.mli
+++ b/matita/components/grafite_parser/grafiteDisambiguate.mli
@@ -25,14 +25,14 @@
 
 exception BaseUriNotSetYet
 
-class g_status :
-  object
+class type g_status =
+ object
   inherit LexiconEngine.g_status
   inherit NCicCoercion.g_status
-  end
+ end
 
 class status :
- object
+ object ('self)
   inherit LexiconEngine.status
   inherit NCicCoercion.status
   method set_grafite_disambiguate_status: #g_status -> 'self

diff --git a/matita/components/ng_library/nCicLibrary.ml b/matita/components/ng_library/nCicLibrary.ml
index d4ea77a317ba7be499218c693ed028c62bd8dfae..70be8ae5768c31cf13bdc2c7e75a63dda843cf7c 100644 (file)
--- a/matita/components/ng_library/nCicLibrary.ml
+++ b/matita/components/ng_library/nCicLibrary.ml
@@ -146,19 +146,11 @@ let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps=
 
 let init = load_db;;
 
-class type g_status =
- object
-  method timestamp: timestamp
- end
-
 class status =
  object(self)
   val timestamp = (time0 : timestamp)
   method timestamp = timestamp
   method set_timestamp v = {< timestamp = v >}
-  method set_library_status
-   : 'status. #g_status as 'status -> 'self
-   = fun o -> self#set_timestamp o#timestamp
  end
 
 let time_travel status =

diff --git a/matita/components/ng_library/nCicLibrary.mli b/matita/components/ng_library/nCicLibrary.mli
index de53755f46b674d6cf4d6601723b1c15a91451bc..bad0d89752eddcaa92658a49cde7ee51614901e7 100644 (file)
--- a/matita/components/ng_library/nCicLibrary.mli
+++ b/matita/components/ng_library/nCicLibrary.mli
@@ -15,16 +15,10 @@ exception LibraryOutOfSync of string Lazy.t
 
 type timestamp
 
-class type g_status =
- object
-  method timestamp: timestamp
- end
-
 class status :
  object ('self)
-  inherit g_status
+  method timestamp: timestamp
   method set_timestamp: timestamp -> 'self
-  method set_library_status: #g_status -> 'self
  end
 
 (* it also checks it and add it to the environment *)

diff --git a/matita/components/ng_tactics/nTactics.ml b/matita/components/ng_tactics/nTactics.ml
index ac3dd00b7fa3b776ff4b139068e05ed7e5d93f77..331945819395f95db65665d46236b6b1629abb0f 100644 (file)
--- a/matita/components/ng_tactics/nTactics.ml
+++ b/matita/components/ng_tactics/nTactics.ml
@@ -205,10 +205,10 @@ let compare_statuses ~past ~present =
 let exec tac (low_status : #lowtac_status) g =
   let stack = [ [0,Open g], [], [], `NoTag ] in
   let status =
-   (new NTacStatus.status low_status#obj stack)#set_estatus low_status
+   (new NTacStatus.status low_status#obj stack)#set_pstatus low_status
   in
   let status = tac status in
-   (low_status#set_estatus status)#set_obj status#obj
+   (low_status#set_pstatus status)#set_obj status#obj
 ;;
 
 let distribute_tac tac (status : #tac_status) =
@@ -236,7 +236,7 @@ let distribute_tac tac (status : #tac_status) =
             in
             aux s go gc loc_tl
       in
-      let s0 = (new NTacStatus.status status#obj ())#set_estatus status in
+      let s0 = (new NTacStatus.status status#obj ())#set_pstatus status in
       let s0, go0, gc0 = s0, [], [] in
       let sn, gon, gcn = aux s0 go0 gc0 g in
       debug_print (lazy ("opened: "
@@ -246,7 +246,7 @@ let distribute_tac tac (status : #tac_status) =
       let stack =
         (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s
       in
-       ((status#set_stack stack)#set_obj(sn:>lowtac_status)#obj)#set_estatus sn
+       ((status#set_stack stack)#set_obj(sn:>lowtac_status)#obj)#set_pstatus sn
 ;;
 
 let atomic_tac htac: #tac_status as 'a -> 'a = distribute_tac (exec htac) ;;

diff --git a/matita/components/statuses.txt b/matita/components/statuses.txt
index 8e47b67f0e071c19d2b804627b82e762ea4dd55e..cb454ba5c78471b185eaa810919ac01d7203599d 100644 (file)
--- a/matita/components/statuses.txt
+++ b/matita/components/statuses.txt
@@ -1,7 +1,7 @@
-grafitetypes -> tac -> auto + eq + (grafitedisambiguate = lexicon +nciccoercion)
-           |--> dumpable                                    |
-           |--> nciclibrary                             interpretation
+grafitetypes -> tac -> auto + eq + (grafitedisambiguate = lexicon+nciccoercion)
+           |--> dumpable                                    |             |
+           |--> nciclibrary                             interpretation unif_hint
 
-ntermciccontent -> nciccoercion+interpretation
+ntermciccontent = nciccoercion+interpretation
                        |
                   unif_hint

diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index ef685c5950f10408ed1f16d094f4d650f04005c0..5cf0ad95d8ec2892faf9bdaa1022d1f4fbfea23b 100644 (file)
--- a/matita/matita/matitaEngine.ml
+++ b/matita/matita/matitaEngine.ml
@@ -30,13 +30,6 @@ module G = GrafiteAst
 let debug = false ;;
 let debug_print = if debug then prerr_endline else ignore ;;
 
-let disambiguate_command lexicon_status_ref grafite_status cmd =
- let lexicon_status,cmd =
-  GrafiteDisambiguate.disambiguate_command !lexicon_status_ref cmd
- in
-  lexicon_status_ref := lexicon_status;
-  grafite_status,cmd
-
 let eval_macro_screenshot (status : GrafiteTypes.status) name =
   assert false (* MATITA 1.0
   let _,_,metasenv,subst,_ = status#obj in
@@ -63,9 +56,7 @@ let eval_ast ?do_heavy_checks status (text,prefix_len,ast) =
  let lexicon_status_ref = ref (status :> LexiconEngine.status) in
  let baseuri = status#baseuri in
  let new_status,new_objs =
-  GrafiteEngine.eval_ast
-   ~disambiguate_command:(disambiguate_command lexicon_status_ref)
-   ?do_heavy_checks status (text,prefix_len,ast)
+  GrafiteEngine.eval_ast ?do_heavy_checks status (text,prefix_len,ast)
  in
  let new_status =
   if !lexicon_status_ref#lstatus != status#lstatus then

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index 6d4c8c0f5601173583b9c36d4e1969df086def4b..7f2cb952c859176423d1577b3e734dff86359f0f 100644 (file)
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -81,7 +81,7 @@ let save_moo grafite_status =
      in
      LexiconMarshal.save_lexicon lexicon_fname
       grafite_status#lstatus.LexiconEngine.lexicon_content_rev;
-     NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
+     GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
       grafite_status#dump
   | _ -> clean_current_baseuri grafite_status 
 ;;
@@ -856,12 +856,14 @@ class gui () =
           | false -> main#toplevel#unfullscreen ());
       main#fullscreenMenuItem#set_active false;
       MatitaGtkMisc.toggle_callback ~check:main#ppNotationMenuItem
-        ~callback:(function
-          | true ->
-              CicNotation.set_active_notations
-                (List.map fst (CicNotation.get_all_notations ()))
-          | false ->
-              CicNotation.set_active_notations []);
+        ~callback:(
+          let s = s () in
+          let status =
+           Interpretations.toggle_active_interpretations s#grafite_status
+          in
+           assert false (* MATITA1.0 ???
+           s#set_grafite_status status*)
+         );
       MatitaGtkMisc.toggle_callback ~check:main#hideCoercionsMenuItem
         ~callback:(fun enabled -> NTermCicContent.hide_coercions := enabled);
       MatitaGtkMisc.toggle_callback ~check:main#unicodeAsTexMenuItem

diff --git a/matita/matita/matitaGuiTypes.mli b/matita/matita/matitaGuiTypes.mli
index 7fc6f9ae56280ec1827307a8b89564482e44d53c..64dd3cd6f1a69927e7cd8417836c9e7c16a3792d 100644 (file)
--- a/matita/matita/matitaGuiTypes.mli
+++ b/matita/matita/matitaGuiTypes.mli
@@ -131,9 +131,9 @@ object
 
     (** load a sequent and render it into parent widget *)
   method nload_sequent:
-   #NCicCoercion.status -> NCic.metasenv -> NCic.substitution -> int -> unit
+   #NTermCicContent.status -> NCic.metasenv -> NCic.substitution -> int -> unit
 
-  method load_nobject: #NCicCoercion.status -> NCic.obj -> unit
+  method load_nobject: #NTermCicContent.status -> NCic.obj -> unit
 end
 
 class type sequentsViewer =
@@ -143,7 +143,7 @@ object
   method load_logo_with_qed: unit
   method nload_sequents: #NTacStatus.tac_status -> unit
   method goto_sequent:
-   #NCicCoercion.status -> int -> unit (* to be called _after_ load_sequents *)
+   #NTermCicContent.status -> int -> unit (* to be called _after_ load_sequents *)
 
   method cicMathView: cicMathView
 end

diff --git a/matita/matita/matitacLib.ml b/matita/matita/matitacLib.ml
index 8ab5d407f8b55d4c30b6936e72cd5229712c6263..cc0793c96b9d0f94f9d444affd72751c37f020fc 100644 (file)
--- a/matita/matita/matitacLib.ml
+++ b/matita/matita/matitacLib.ml
@@ -231,7 +231,7 @@ let compile atstart options fname =
      (if Helm_registry.get_bool "matita.moo" then begin
         (* FG: we do not generate .moo when dumping .mma files *)
         LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
-        NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
+        GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
          grafite_status#dump
      end;
      let tm = Unix.gmtime elapsed in