attributes now in the proof status: commit 1

diff --git a/matita/matita.ml b/matita/matita.ml
index 5a638b48d79bb86fd39188b0c9cbe753aead9e63..46926ea9b387e75a32d0d9c213030136459485d2 100644 (file)
--- a/matita/matita.ml
+++ b/matita/matita.ml
@@ -167,8 +167,8 @@ let _ =
             (MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status
             with
             | GrafiteTypes.No_proof -> (Cic.Implicit None)
-            | Incomplete_proof i -> let _,_,p,_ = i.GrafiteTypes.proof in p
-            | Proof p -> let _,_,p,_ = p in p
+            | Incomplete_proof i -> let _,_,p,_, _ = i.GrafiteTypes.proof in p
+            | Proof p -> let _,_,p,_, _ = p in p
             | Intermediate _ -> assert false)));
      addDebugItem "Print current proof (natural language) to stderr" 
        (fun _ -> 
@@ -179,10 +179,10 @@ let _ =
             with
             | GrafiteTypes.No_proof -> assert false
             | Incomplete_proof i -> 
-                let _,m,p,ty = i.GrafiteTypes.proof in 
-                Cic.CurrentProof ("current (incomplete) proof",m,p,ty,[],[])
-            | Proof (_,m,p,ty) -> 
-                Cic.CurrentProof ("current proof",m,p,ty,[],[])
+                let _,m,p,ty, attrs = i.GrafiteTypes.proof in 
+                Cic.CurrentProof ("current (incomplete) proof",m,p,ty,[],attrs)
+            | Proof (_,m,p,ty, attrs) -> 
+                Cic.CurrentProof ("current proof",m,p,ty,[],attrs)
             | Intermediate _ -> assert false)));
 (*     addDebugItem "ask record choice"
       (fun _ ->

diff --git a/matita/matitaMathView.ml b/matita/matitaMathView.ml
index ee49267fe3c57d1579fb2924dd07dc4c7e1c0150..c32c00f203c12c4fa99dad0730cdd3b79335bae0 100644 (file)
--- a/matita/matitaMathView.ml
+++ b/matita/matitaMathView.ml
@@ -648,7 +648,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
       _metasenv <- []; 
       self#script#setGoal None
 
-    method load_sequents { proof = (_,metasenv,_,_) as proof; stack = stack } =
+    method load_sequents { proof = (_,metasenv,_,_, _) as proof; stack = stack } =
       _metasenv <- metasenv;
       pages <- 0;
       let win goal_switch =
@@ -1090,13 +1090,13 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     method private home () =
       self#_showMath;
       match self#script#grafite_status.proof_status with
-      | Proof  (uri, metasenv, bo, ty) ->
+      | Proof  (uri, metasenv, bo, ty, attrs) ->
           let name = UriManager.name_of_uri (HExtlib.unopt uri) in
-          let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
+          let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], attrs) in
           self#_loadObj obj
-      | Incomplete_proof { proof = (uri, metasenv, bo, ty) } ->
+      | Incomplete_proof { proof = (uri, metasenv, bo, ty, attrs) } ->
           let name = UriManager.name_of_uri (HExtlib.unopt uri) in
-          let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
+          let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], attrs) in
           self#_loadObj obj
       | _ -> self#blank ()
 

diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml
index 7a978bbde3bb19fdd2d0b6eb7d1de28fa17b0831..4c35019bca8308c408b8462be9255a2a68cab40d 100644 (file)
--- a/matita/matitaScript.ml
+++ b/matita/matitaScript.ml
@@ -234,7 +234,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
      [], "", parsed_text_length
   | TA.WHint (loc, term) ->
-     let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in
+     let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term, []),0) in
      let l = List.map fst (MQ.experimental_hint ~dbd s) in
      let entry = `Whelp (pp_macro mac, l) in
      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
@@ -332,7 +332,7 @@ prerr_endline ("Stampo " ^ UriManager.string_of_uri uri);
               (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri))
             with
             | e (* BRRRRRRRRR *) -> 
-               Printf.sprintf "\nERRORE IN STAMPA DI %s\n%s\n" 
+               Printf.sprintf "\n(* ERRORE IN STAMPA DI %s\nEXCEPTION: %s *)\n" 
                (UriManager.string_of_uri uri) (Printexc.to_string e)
           ) sorted_uris_without_xpointer)
       in