From e3c0cc9893402419e363ad6616a599f194438273 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 21 Jan 2005 09:40:48 +0000 Subject: [PATCH] snapshot, notably: - attributes support - new ApplyTransformation interface - simil-coma commit, browser is partially implemented :( --- helm/matita/buildTimeConf.ml.in | 2 +- helm/matita/matita.conf.xml.sample | 4 +-- helm/matita/matita.glade | 41 ++++++++++---------------- helm/matita/matita.ml | 4 ++- helm/matita/matitaCicMisc.ml | 4 +-- helm/matita/matitaGeneratedGui.ml | 16 +++++----- helm/matita/matitaGeneratedGui.mli | 8 ++--- helm/matita/matitaGui.ml | 1 + helm/matita/matitaGui.mli | 1 + helm/matita/matitaInterpreter.ml | 25 +++++++++------- helm/matita/matitaMathView.ml | 47 +++++++++++++++++++++--------- helm/matita/matitaMathView.mli | 19 +++++++++--- helm/matita/matitac.ml | 7 +++-- 13 files changed, 105 insertions(+), 74 deletions(-) diff --git a/helm/matita/buildTimeConf.ml.in b/helm/matita/buildTimeConf.ml.in index 39efbf62b..e75988386 100644 --- a/helm/matita/buildTimeConf.ml.in +++ b/helm/matita/buildTimeConf.ml.in @@ -29,5 +29,5 @@ let undo_history_size = 10;; let console_history_size = 100;; let gtkrc = "@MATITA_GTKRC@";; let base_uri = "cic:/matita";; -let phrase_sep = ";;";; +let phrase_sep = ".";; diff --git a/helm/matita/matita.conf.xml.sample b/helm/matita/matita.conf.xml.sample index 6aee8a561..9035d2a78 100644 --- a/helm/matita/matita.conf.xml.sample +++ b/helm/matita/matita.conf.xml.sample @@ -1,8 +1,8 @@
- - localhost + mowgli.cs.unibo.it +
matita.glade diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 12b772a95..58c713292 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -2262,6 +2262,8 @@ Copyright (C) 2004, + 400 + 500 Cic browser GTK_WINDOW_TOPLEVEL GTK_WIN_POS_NONE @@ -2457,36 +2459,25 @@ Copyright (C) 2004, - + True - True - True - True - GTK_POS_TOP - False - False - - - - + 0 + 0 + GTK_SHADOW_NONE - + True - current proof - False - False - GTK_JUSTIFY_LEFT - False - False - 0.5 - 0.5 - 0 - 0 + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT + + + + - - tab - diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 107691932..13ec23a6e 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -88,6 +88,7 @@ let _ = (* attach observers to proof status *) currentProof#connect `Abort (fun () -> sequents_viewer#reset; false) let mathViewer = MatitaMathView.mathViewer () +let cicBrowser = MatitaMathView.cicBrowser () let interpreter = let console = (gui#console :> MatitaTypes.console) in let currentProof = (currentProof :> MatitaTypes.currentProof) in @@ -213,7 +214,8 @@ let _ = let i = ref 0 in List.iter (fun t -> incr i; debug_print (sprintf "%d: %s" !i (CicPp.ppterm t))) - sequent_viewer#get_selected_terms) + sequent_viewer#get_selected_terms); + addDebugItem "show cic browser" (fun () -> gui#browser#browserWin#show ()); end (** *) diff --git a/helm/matita/matitaCicMisc.ml b/helm/matita/matitaCicMisc.ml index 523e33ea2..c77ded6be 100644 --- a/helm/matita/matitaCicMisc.ml +++ b/helm/matita/matitaCicMisc.ml @@ -27,11 +27,11 @@ let cicCurrentProof (uri, metasenv, bo, ty) = let uri = MatitaTypes.unopt_uri uri in (* TODO CSC: Wrong: [] is just plainly wrong *) - Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []) + Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, [], []) (** create a Cic.Constant from a given proof *) let cicConstant (uri, metasenv, bo, ty) = let uri = MatitaTypes.unopt_uri uri in (* TODO CSC: Wrong: [] is just plainly wrong *) - Cic.Constant (UriManager.name_of_uri uri, Some bo, ty, []) + Cic.Constant (UriManager.name_of_uri uri, Some bo, ty, [], []) diff --git a/helm/matita/matitaGeneratedGui.ml b/helm/matita/matitaGeneratedGui.ml index e9db307d4..689984774 100644 --- a/helm/matita/matitaGeneratedGui.ml +++ b/helm/matita/matitaGeneratedGui.ml @@ -841,14 +841,14 @@ class browserWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GMisc.image (GtkMisc.Image.cast (Glade.get_widget_msg ~name:"image187" ~info:"GtkImage" xmldata)) method image187 = image187 - val browserNotebook = - new GPack.notebook (GtkPack.Notebook.cast - (Glade.get_widget_msg ~name:"BrowserNotebook" ~info:"GtkNotebook" xmldata)) - method browserNotebook = browserNotebook - val label9 = - new GMisc.label (GtkMisc.Label.cast - (Glade.get_widget_msg ~name:"label9" ~info:"GtkLabel" xmldata)) - method label9 = label9 + val frame1 = + new GBin.frame (GtkBin.Frame.cast + (Glade.get_widget_msg ~name:"frame1" ~info:"GtkFrame" xmldata)) + method frame1 = frame1 + val scrolledBrowser = + new GBin.scrolled_window (GtkBin.ScrolledWindow.cast + (Glade.get_widget_msg ~name:"ScrolledBrowser" ~info:"GtkScrolledWindow" xmldata)) + method scrolledBrowser = scrolledBrowser method reparent parent = browserWinEventBox#misc#reparent parent; toplevel#destroy () diff --git a/helm/matita/matitaGeneratedGui.mli b/helm/matita/matitaGeneratedGui.mli index 113538361..a84c1328a 100644 --- a/helm/matita/matitaGeneratedGui.mli +++ b/helm/matita/matitaGeneratedGui.mli @@ -487,9 +487,9 @@ class browserWin : val browserBackButton : GButton.button val browserForwardButton : GButton.button val browserHomeButton : GButton.button - val browserNotebook : GPack.notebook val browserWin : GWindow.window val browserWinEventBox : GBin.event_box + val frame1 : GBin.frame val hbox6 : GPack.box val hbox7 : GPack.box val image187 : GMisc.image @@ -497,7 +497,7 @@ class browserWin : val image189 : GMisc.image val image190 : GMisc.image val label10 : GMisc.label - val label9 : GMisc.label + val scrolledBrowser : GBin.scrolled_window val toplevel : GWindow.window val vbox7 : GPack.box val xml : Glade.glade_xml Gtk.obj @@ -506,10 +506,10 @@ class browserWin : method browserBackButton : GButton.button method browserForwardButton : GButton.button method browserHomeButton : GButton.button - method browserNotebook : GPack.notebook method browserWin : GWindow.window method browserWinEventBox : GBin.event_box method check_widgets : unit -> unit + method frame1 : GBin.frame method hbox6 : GPack.box method hbox7 : GPack.box method image187 : GMisc.image @@ -517,8 +517,8 @@ class browserWin : method image189 : GMisc.image method image190 : GMisc.image method label10 : GMisc.label - method label9 : GMisc.label method reparent : GObj.widget -> unit + method scrolledBrowser : GBin.scrolled_window method toplevel : GWindow.window method vbox7 : GPack.box method xml : Glade.glade_xml Gtk.obj diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index f8f252b52..de5240e44 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -123,6 +123,7 @@ class gui file = *) method about = about + method browser = browser method check = check method console = console method fileSel = fileSel diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli index 39657c587..419dc77eb 100644 --- a/helm/matita/matitaGui.mli +++ b/helm/matita/matitaGui.mli @@ -34,6 +34,7 @@ class gui : (** {2 Access to lower-level GTK widgets} *) method about : MatitaGeneratedGui.aboutWin + method browser : MatitaGeneratedGui.browserWin method check : MatitaGeneratedGui.checkWin method fileSel : MatitaGeneratedGui.fileSelectionWin method main : MatitaGeneratedGui.mainWin diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml index bb43d67e0..b891f4e94 100644 --- a/helm/matita/matitaInterpreter.ml +++ b/helm/matita/matitaInterpreter.ml @@ -54,8 +54,8 @@ let qualify name = else String.concat "/" [baseuri; name] let split_obj = function - | Cic.Constant (name, body, ty, _) - | Cic.Variable (name, body, ty, _) -> (name, body, ty) + | Cic.Constant (name, body, ty, _, attrs) + | Cic.Variable (name, body, ty, _, attrs) -> (name, body, ty, attrs) | _ -> assert false let canonical_context metano metasenv = @@ -260,9 +260,9 @@ let inddef_of_ast params indTypes (disambiguator:MatitaTypes.disambiguator) = * - save object to disk in xml format * - register uri to the getter * - save universe file *) -let add_constant_to_world ~dbd ~uri ?body ~ty ~ugraph () = +let add_constant_to_world ~dbd ~uri ?body ~ty ?(attrs = []) ~ugraph () = let name = UriManager.name_of_uri uri in - let obj = Cic.Constant (name, body, ty, []) in + let obj = Cic.Constant (name, body, ty, [], attrs) in let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in CicEnvironment.add_type_checked_term uri (obj, ugraph); MetadataDb.index_constant ~dbd @@ -316,7 +316,7 @@ class commandState let (uri, (indTypes, params, leftno)) = inddef_of_ast params indTypes disambiguator in - let obj = Cic.InductiveDefinition (indTypes, params, leftno) in + let obj = Cic.InductiveDefinition (indTypes, params, leftno, []) in let ugraph = CicTypeChecker.typecheck_mutual_inductive_defs uri (indTypes, params, leftno) CicUniv.empty_ugraph @@ -325,20 +325,21 @@ class commandState CicEnvironment.put_inductive_definition uri (obj, ugraph); MetadataDb.index_inductive_def ~dbd ~owner:(Helm_registry.get "matita.owner") ~uri ~types:indTypes; - let msgs = ref [] in let elim sort = try let obj = CicElim.elim_of ~sort uri 0 in - let (name, body, ty) = split_obj obj in - let uri = UriManager.uri_of_string (qualify name ^ ".con") in + let (name, body, ty, attrs) = split_obj obj in + let suri = qualify name ^ ".con" in + let uri = UriManager.uri_of_string suri in (* TODO Zack: make CicElim returns a universe *) let ugraph = CicUniv.empty_ugraph in - add_constant_to_world ~dbd ~uri ?body ~ty ~ugraph (); - msgs := (sprintf "%s defined" name) :: !msgs; + add_constant_to_world ~dbd ~uri ?body ~ty ~attrs ~ugraph (); + console#echo_message + (sprintf "%s eliminator (automatically) defined" suri) with CicElim.Can_t_eliminate -> () in List.iter elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ]; - Echo (String.concat "\n" (List.rev !msgs)) + Quiet | TacticAst.Command TacticAst.Quit -> currentProof#quit (); New_state Command (* dummy answer, useless *) @@ -441,6 +442,7 @@ class proofState let proof = currentProof#proof in let (uri, metasenv, bo, ty) = proof#proof in let uri = MatitaTypes.unopt_uri uri in + let suri = UriManager.string_of_uri uri in (* TODO Zack this function probably should not simply fail with * Failure, but rather raise some more meaningful exception *) if metasenv <> [] then failwith "Proof not completed"; @@ -454,6 +456,7 @@ class proofState add_constant_to_world ~dbd ~uri ~body:bo ~ty ~ugraph (); currentProof#abort (); (match mathViewer with None -> () | Some v -> v#unload ()); + console#echo_message (sprintf "%s defined" suri); New_state Command | TacticAst.Seq tacticals -> (* TODO Zack check for proof completed at each step? *) diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index f264ec413..03803c2b9 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -85,8 +85,17 @@ class clickable_math_view obj = | None -> self#set_selection None end +let clickable_math_view = + GtkBase.Widget.size_params + ~cont:(OgtkMathViewProps.pack_return (fun p -> + OgtkMathViewProps.set_params + (new clickable_math_view (GtkMathViewProps.MathView_GMetaDOM.create p)) + ~font_size:None ~log_verbosity:None)) + [] +let clickable_math_view () = clickable_math_view () + class proof_viewer obj = - object(self) + object (self) inherit clickable_math_view obj @@ -94,16 +103,14 @@ class proof_viewer obj = val mutable current_mathml = None method load_proof ((uri_opt, _, _, _) as proof, (goal_opt: int option)) = - let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, - ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) = - Cic2acic.acic_object_of_cic_object (cicCurrentProof proof) + let uri = unopt_uri uri_opt in + let obj = cicCurrentProof proof in + let (mathml, (ids_to_terms, ids_to_father_ids, ids_to_conjectures, + ids_to_hypotheses)) = + ApplyTransformation.mml_of_cic_object uri obj in current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses); - let mathml = - ApplyTransformation.mml_of_cic_object ~explode_all:true - (unopt_uri uri_opt) annobj ids_to_inner_sorts ids_to_inner_types - in debug_print "load_proof: dumping MathML to ./proof"; ignore (Misc.domImpl#saveDocumentToFile ~name:"./proof" ~doc:mathml ()); match current_mathml with @@ -269,6 +276,18 @@ let sequent_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity = ~font_size ~log_verbosity)) [] +class cicBrowser = + object (self) + val widget = + let gui = MatitaGui.instance () in + sequent_viewer ~show:true ~packing:gui#browser#scrolledBrowser#add () + + initializer + widget#set_href_callback (Some (fun uri -> self#load_uri uri)) + + method load_uri uri = () + end + let proof_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity = GtkBase.Widget.size_params ~cont:(OgtkMathViewProps.pack_return (fun p -> @@ -284,11 +303,6 @@ let proof_viewer_instance = ) in fun () -> Lazy.force instance -let sequents_viewer ~(notebook:GPack.notebook) - ~(sequent_viewer:sequent_viewer) ~set_goal () -= - new sequents_viewer ~notebook ~sequent_viewer ~set_goal () - class mathViewer = let href_callback: (UriManager.uri -> unit) option ref = ref None in object @@ -314,5 +328,12 @@ class mathViewer = method unload () = (proof_viewer_instance ())#unload end +let sequents_viewer ~(notebook:GPack.notebook) + ~(sequent_viewer:sequent_viewer) ~set_goal () += + new sequents_viewer ~notebook ~sequent_viewer ~set_goal () + let mathViewer () = new mathViewer +let cicBrowser () = new cicBrowser + diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli index 04d96befe..8b5ca89ac 100644 --- a/helm/matita/matitaMathView.mli +++ b/helm/matita/matitaMathView.mli @@ -64,6 +64,13 @@ class type sequents_viewer = method goto_sequent: int -> unit (* to be called _after_ load_sequents *) end +class type cicBrowser = + object + method load_uri: UriManager.uri -> unit + end + +(** {2 Constructors} *) + val proof_viewer: ?hadjustment:GData.adjustment -> ?vadjustment:GData.adjustment -> @@ -76,10 +83,6 @@ val proof_viewer: unit -> proof_viewer - (** singleton proof_viewer instance. - * Uses singleton GUI instance *) -val proof_viewer_instance: unit -> proof_viewer - val sequent_viewer: ?hadjustment:GData.adjustment -> ?vadjustment:GData.adjustment -> @@ -99,5 +102,13 @@ val sequents_viewer: unit -> sequents_viewer +val cicBrowser: unit -> cicBrowser + val mathViewer: unit -> MatitaTypes.mathViewer +(** {2 Singletons} *) + + (** singleton proof_viewer instance. + * Uses singleton GUI instance *) +val proof_viewer_instance: unit -> proof_viewer + diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml index 648702490..3f394cdb1 100644 --- a/helm/matita/matitac.ml +++ b/helm/matita/matitac.ml @@ -84,7 +84,7 @@ let interpreter = ~disambiguator ~currentProof ~console ~dbd () let run_script fname = - message (sprintf "execution of %s started." fname); + message (sprintf "execution of %s started:" fname); let script = let ic = open_in fname in let ast = snd (CicTextualParser2.parse_script (Stream.of_channel ic)) in @@ -92,7 +92,7 @@ let run_script fname = ast in let rec aux = function - | [] -> () + | [] -> () (* script is over *) | DisambiguateTypes.Comment _ :: tl -> aux tl | DisambiguateTypes.Command ast :: tl -> let loc = @@ -107,7 +107,8 @@ let run_script fname = else aux tl in - aux script + aux script; + message (sprintf "execution of %s completed." fname) let _ = List.iter run_script scripts -- 2.39.2