X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=addf9763cc2350125be11b57792f8d41d1a5f506;hb=de9a83f286eee12117fb478ea2db18f7faebac9a;hp=7aa54f2c74ed03a3407bc4b4d18e5165f67c6da3;hpb=393b5943416585d0612ec62b795ceee34adb8dd7;p=helm.git diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 7aa54f2c7..addf9763c 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2000-2002, HELM Team. +(* Copyright (C) 2004-2005, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -25,26 +25,27 @@ open Printf -open MatitaCicMisc open MatitaTypes -(* List utility functions *) -exception Skip - let list_map_fail f = - let rec aux = - function - [] -> [] - | he::tl -> - try - let he' = f he in - he'::(aux tl) - with Skip -> - (aux tl) - in + let rec aux = function + | [] -> [] + | he::tl -> + try + let he' = f he in + he'::(aux tl) + with Exit -> + (aux tl) + in aux -class clickable_math_view obj = +(** inherit from this class if you want to access current script *) +class scriptAccessor = +object (self) + method private script = MatitaScript.instance () +end + +class clickableMathView obj = let href = Gdome.domString "href" in let xref = Gdome.domString "xref" in object (self) @@ -85,18 +86,18 @@ class clickable_math_view obj = | None -> self#set_selection None end -let clickable_math_view ?hadjustment ?vadjustment ?font_size ?log_verbosity = +let clickableMathView ?hadjustment ?vadjustment ?font_size ?log_verbosity = GtkBase.Widget.size_params ~cont:(OgtkMathViewProps.pack_return (fun p -> OgtkMathViewProps.set_params - (new clickable_math_view (GtkMathViewProps.MathView_GMetaDOM.create p)) + (new clickableMathView (GtkMathViewProps.MathView_GMetaDOM.create p)) ~font_size:None ~log_verbosity:None)) [] -class sequent_viewer obj = +class sequentViewer obj = object(self) - inherit clickable_math_view obj + inherit clickableMathView obj val mutable current_infos = None @@ -113,9 +114,7 @@ class sequent_viewer obj = else match current_infos with | Some (ids_to_terms,_,_) -> - (try - Hashtbl.find ids_to_terms xpath - with _ -> raise Skip) + (try Hashtbl.find ids_to_terms xpath with _ -> raise Exit) | None -> assert false) (* "ERROR: No current term!!!" *) selections @@ -132,9 +131,7 @@ class sequent_viewer obj = else match current_infos with | Some (_,_,ids_to_hypotheses) -> - (try - Hashtbl.find ids_to_hypotheses xpath - with _ -> raise Skip) + (try Hashtbl.find ids_to_hypotheses xpath with _ -> raise Exit) | None -> assert false) (* "ERROR: No current term!!!" *) selections @@ -151,19 +148,12 @@ class sequent_viewer obj = self#load_root ~root:mathml#get_documentElement end - -class sequents_viewer ~(notebook:GPack.notebook) - ~(sequent_viewer:sequent_viewer) () +class sequentsViewer ~(notebook:GPack.notebook) + ~(sequentViewer:sequentViewer) () = - let tab_label metano = - (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce - in - let set_goal goal = - let currentProof = MatitaProof.instance () in - assert (currentProof#onGoing ()); - currentProof#proof#set_goal goal - in object (self) + inherit scriptAccessor + val mutable pages = 0 val mutable switch_page_callback = None val mutable page2goal = [] (* associative list: page no -> goal no *) @@ -171,14 +161,17 @@ class sequents_viewer ~(notebook:GPack.notebook) val mutable goal2win = [] (* associative list: goal no -> scrolled win *) val mutable _metasenv = [] val mutable scrolledWin: GBin.scrolled_window option = None - (* scrolled window to which the sequent_viewer is currently attached *) + (* scrolled window to which the sequentViewer is currently attached *) + + method private tab_label metano = + (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce method reset = (match scrolledWin with | Some w -> (* removing page from the notebook will destroy all contained widget, - * we do not want the sequent_viewer to be destroyed as well *) - w#remove sequent_viewer#coerce; + * we do not want the sequentViewer to be destroyed as well *) + w#remove sequentViewer#coerce; scrolledWin <- None | None -> ()); for i = 1 to pages do notebook#remove_page 0 done; @@ -187,16 +180,19 @@ class sequents_viewer ~(notebook:GPack.notebook) goal2page <- []; goal2win <- []; _metasenv <- []; + self#script#setGoal ~-1; (match switch_page_callback with | Some id -> GtkSignal.disconnect notebook#as_widget id; switch_page_callback <- None | None -> ()) - method load_sequents metasenv = + method load_sequents (status: ProofEngineTypes.status) = + let ((_, metasenv, _, _), goal) = status in let sequents_no = List.length metasenv in _metasenv <- metasenv; pages <- sequents_no; + self#script#setGoal goal; let win metano = let w = GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC @@ -204,9 +200,9 @@ class sequents_viewer ~(notebook:GPack.notebook) in let reparent () = scrolledWin <- Some w; - match sequent_viewer#misc#parent with - | None -> w#add sequent_viewer#coerce - | Some _ -> sequent_viewer#misc#reparent w#coerce + match sequentViewer#misc#parent with + | None -> w#add sequentViewer#coerce + | Some _ -> sequentViewer#misc#reparent w#coerce in goal2win <- (metano, reparent) :: goal2win; w#coerce @@ -217,7 +213,7 @@ class sequents_viewer ~(notebook:GPack.notebook) page2goal <- (!page, metano) :: page2goal; goal2page <- (metano, !page) :: goal2page; incr page; - notebook#append_page ~tab_label:(tab_label metano) (win metano)) + notebook#append_page ~tab_label:(self#tab_label metano) (win metano)) metasenv; switch_page_callback <- Some (notebook#connect#switch_page ~callback:(fun page -> @@ -226,14 +222,14 @@ class sequents_viewer ~(notebook:GPack.notebook) List.assoc page page2goal with Not_found -> assert false in - set_goal goal; + self#script#setGoal goal; self#render_page ~page ~goal)) method private render_page ~page ~goal = - sequent_viewer#load_sequent _metasenv goal; + sequentViewer#load_sequent _metasenv goal; try List.assoc goal goal2win (); - sequent_viewer#set_selection None + sequentViewer#set_selection None with Not_found -> assert false method goto_sequent goal = @@ -261,28 +257,40 @@ type 'widget constructor = unit -> 'widget -let sequent_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity = +let sequentViewer ?hadjustment ?vadjustment ?font_size ?log_verbosity = GtkBase.Widget.size_params ~cont:(OgtkMathViewProps.pack_return (fun p -> OgtkMathViewProps.set_params - (new sequent_viewer (GtkMathViewProps.MathView_GMetaDOM.create p)) + (new sequentViewer (GtkMathViewProps.MathView_GMetaDOM.create p)) ~font_size ~log_verbosity)) [] let blank_uri = BuildTimeConf.blank_uri let current_proof_uri = BuildTimeConf.current_proof_uri +type term_source = + [ `Ast of DisambiguateTypes.term + | `Cic of Cic.term * Cic.metasenv + | `String of string + ] + exception Browser_failure of string let cicBrowsers = ref [] -class cicBrowser ~(history:string MatitaMisc.history) () = +class type cicBrowser = +object + method loadUri: string -> unit + method loadTerm: term_source -> unit +end + +class cicBrowser_impl ~(history:string MatitaMisc.history) () = let term_RE = Pcre.regexp "^term:(.*)" in let trailing_slash_RE = Pcre.regexp "/$" in let gui = MatitaGui.instance () in let win = gui#newBrowserWin () in let toplevel = win#toplevel in - let mathView = sequent_viewer ~packing:win#scrolledBrowser#add () in + let mathView = sequentViewer ~packing:win#scrolledBrowser#add () in let fail msg = ignore (MatitaGtkMisc.ask_confirmation ~gui:(MatitaGui.instance ()) ~title:"Cic browser" ~msg ~cancel:false ()); @@ -295,6 +303,8 @@ class cicBrowser ~(history:string MatitaMisc.history) () = in let handle_error' f = fun () -> handle_error f in (* used in callbacks *) object (self) + inherit scriptAccessor + initializer ignore (win#browserUri#connect#activate (handle_error' (fun () -> self#_loadUri win#browserUri#text))); @@ -318,9 +328,6 @@ class cicBrowser ~(history:string MatitaMisc.history) () = self#_loadUri ~add_to_history:false blank_uri; toplevel#show (); - val disambiguator = MatitaDisambiguator.instance () - val currentProof = MatitaProof.instance () - val mutable current_uri = "" val mutable current_infos = None val mutable current_mathml = None @@ -363,10 +370,13 @@ class cicBrowser ~(history:string MatitaMisc.history) () = mathView#load_root (MatitaMisc.empty_mathml ())#get_documentElement method private home () = - if currentProof#onGoing () then - self#loadObj (cicCurrentProof currentProof#proof#proof) + if self#script#onGoingProof () then + let ((uri, metasenv, bo, ty), _) = self#script#proofStatus in + let name = UriManager.name_of_uri (MatitaMisc.unopt uri) in + let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in + self#loadObj obj else - raise (Browser_failure "no on going proof") + self#blank () (** loads a cic uri from the environment * @param uri UriManager.uri *) @@ -427,28 +437,28 @@ class cicBrowser ~(history:string MatitaMisc.history) () = mathView#load_root ~root:mathml#get_documentElement; current_mathml <- Some mathml - method private _loadTerm s = - self#_loadTermAst (disambiguator#parserr#parseTerm (Stream.of_string s)) + method private _loadTerm s = failwith "not implemented _loadTerm" +(* TODO self#_loadTermAst (disambiguator#parserr#parseTerm (Stream.of_string s)) *) - method private _loadTermAst ast = - let (_, _, term, _) = + method private _loadTermAst ast = failwith "not implemented _loadTermAst" +(* TODO + let (_, metasenv, term, _) = MatitaCicMisc.disambiguate ~disambiguator ~currentProof ast in - self#_loadTermCic term + self#_loadTermCic term metasenv +*) - method private _loadTermCic term = - let (context, metasenv) = - MatitaCicMisc.get_context_and_metasenv currentProof - in + method private _loadTermCic term metasenv = + let context = self#script#proofContext in let dummyno = CicMkImplicit.new_meta metasenv [] in let sequent = (dummyno, context, term) in mathView#load_sequent (sequent :: metasenv) dummyno - method loadTerm (src:MatitaTypes.term_source) = + method loadTerm (src:term_source) = handle_error (fun () -> (match src with | `Ast ast -> self#_loadTermAst ast - | `Cic cic -> self#_loadTermCic cic + | `Cic (cic, metasenv) -> self#_loadTermCic cic metasenv | `String s -> self#_loadTerm s); self#setUri "check") @@ -463,15 +473,15 @@ class cicBrowser ~(history:string MatitaMisc.history) () = end -let sequents_viewer ~(notebook:GPack.notebook) - ~(sequent_viewer:sequent_viewer) () +let sequentsViewer ~(notebook:GPack.notebook) + ~(sequentViewer:sequentViewer) () = - new sequents_viewer ~notebook ~sequent_viewer () + new sequentsViewer ~notebook ~sequentViewer () let cicBrowser () = let size = BuildTimeConf.browser_history_size in let rec aux history = - let browser = new cicBrowser ~history () in + let browser = new cicBrowser_impl ~history () in let win = browser#win in ignore (win#browserNewButton#connect#clicked (fun () -> let history = @@ -485,27 +495,19 @@ let cicBrowser () = GdkKeysyms._W (fun () -> win#toplevel#destroy ()); *) cicBrowsers := browser :: !cicBrowsers; - (browser :> MatitaTypes.cicBrowser) + (browser :> cicBrowser) in let history = new MatitaMisc.browser_history size blank_uri in aux history let refresh_all_browsers () = List.iter (fun b -> b#refresh ()) !cicBrowsers -class mathViewer = - object - method checkTerm (src:MatitaTypes.term_source) = - (cicBrowser ())#loadTerm src - end - -let mathViewer () = new mathViewer - -let default_sequent_viewer () = sequent_viewer ~show:true () -let sequent_viewer_instance = MatitaMisc.singleton default_sequent_viewer +let default_sequentViewer () = sequentViewer ~show:true () +let sequentViewer_instance = MatitaMisc.singleton default_sequentViewer -let default_sequents_viewer () = +let default_sequentsViewer () = let gui = MatitaGui.instance () in - let sequent_viewer = sequent_viewer_instance () in - sequents_viewer ~notebook:gui#main#sequentsNotebook ~sequent_viewer () -let sequents_viewer_instance = MatitaMisc.singleton default_sequents_viewer + let sequentViewer = sequentViewer_instance () in + sequentsViewer ~notebook:gui#main#sequentsNotebook ~sequentViewer () +let sequentsViewer_instance = MatitaMisc.singleton default_sequentsViewer