From 05078521aaff6f41f55114e5332663b1e9706824 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 10 Jan 2007 14:23:47 +0000 Subject: [PATCH] attributes now in the proof status: commit 1 --- helm/software/matita/matita.ml | 12 ++++++------ helm/software/matita/matitaMathView.ml | 10 +++++----- helm/software/matita/matitaScript.ml | 4 ++-- 3 files changed, 13 insertions(+), 13 deletions(-) diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml index 5a638b48d..46926ea9b 100644 --- a/helm/software/matita/matita.ml +++ b/helm/software/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/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index ee49267fe..c32c00f20 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/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/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index 7a978bbde..4c35019bc 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/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 -- 2.39.2