From b804ff9f8fba300ffaa54add291e0f6490b757ce Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 19 Dec 2010 20:28:10 +0000 Subject: [PATCH] Class mathViewer got rid of. The circular dependency between the scripts needs to be sorted out by putting matitaScript much later in the chain. This commit temporary introduces bad type expressions here and there. --- matita/matita/.depend | 28 ++++++++++++++------------- matita/matita/.depend.opt | 28 ++++++++++++++------------- matita/matita/Makefile | 2 +- matita/matita/cicMathView.ml | 7 ++++--- matita/matita/cicMathView.mli | 5 ++++- matita/matita/matita.ml | 1 - matita/matita/matitaMathView.ml | 33 ++++++++++++++++---------------- matita/matita/matitaMathView.mli | 9 +++++++-- matita/matita/matitaScript.ml | 14 ++++++-------- matita/matita/matitaScript.mli | 1 - matita/matita/matitaTypes.ml | 8 -------- matita/matita/matitaTypes.mli | 5 ----- 12 files changed, 69 insertions(+), 72 deletions(-) diff --git a/matita/matita/.depend b/matita/matita/.depend index d7b9a80a1..0d51469a6 100644 --- a/matita/matita/.depend +++ b/matita/matita/.depend @@ -30,14 +30,14 @@ matitaGui.cmx: virtuals.cmx matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi matitaInit.cmo: matitaExcPp.cmi buildTimeConf.cmo matitaInit.cmi matitaInit.cmx: matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi -matitaMathView.cmo: virtuals.cmi matitaTypes.cmi matitaScript.cmi \ - matitaMisc.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi \ - lablGraphviz.cmi cicMathView.cmi buildTimeConf.cmo \ - applyTransformation.cmi matitaMathView.cmi -matitaMathView.cmx: virtuals.cmx matitaTypes.cmx matitaScript.cmx \ - matitaMisc.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx \ - lablGraphviz.cmx cicMathView.cmx buildTimeConf.cmx \ - applyTransformation.cmx matitaMathView.cmi +matitaMathView.cmo: virtuals.cmi matitaTypes.cmi matitaMisc.cmi \ + matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi lablGraphviz.cmi \ + cicMathView.cmi buildTimeConf.cmo applyTransformation.cmi \ + matitaMathView.cmi +matitaMathView.cmx: virtuals.cmx matitaTypes.cmx matitaMisc.cmx \ + matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx lablGraphviz.cmx \ + cicMathView.cmx buildTimeConf.cmx applyTransformation.cmx \ + matitaMathView.cmi matitaMisc.cmo: matitaGuiTypes.cmi buildTimeConf.cmo matitaMisc.cmi matitaMisc.cmx: matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi matita.cmo: predefined_virtuals.cmi matitaTypes.cmi matitaScript.cmi \ @@ -46,10 +46,12 @@ matita.cmo: predefined_virtuals.cmi matitaTypes.cmi matitaScript.cmi \ matita.cmx: predefined_virtuals.cmx matitaTypes.cmx matitaScript.cmx \ matitaMathView.cmx matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx \ buildTimeConf.cmx -matitaScript.cmo: virtuals.cmi matitaTypes.cmi matitaGtkMisc.cmi \ - matitaEngine.cmi cicMathView.cmi buildTimeConf.cmo matitaScript.cmi -matitaScript.cmx: virtuals.cmx matitaTypes.cmx matitaGtkMisc.cmx \ - matitaEngine.cmx cicMathView.cmx buildTimeConf.cmx matitaScript.cmi +matitaScript.cmo: virtuals.cmi matitaTypes.cmi matitaMathView.cmi \ + matitaGtkMisc.cmi matitaEngine.cmi cicMathView.cmi buildTimeConf.cmo \ + matitaScript.cmi +matitaScript.cmx: virtuals.cmx matitaTypes.cmx matitaMathView.cmx \ + matitaGtkMisc.cmx matitaEngine.cmx cicMathView.cmx buildTimeConf.cmx \ + matitaScript.cmi matitaTypes.cmo: matitaTypes.cmi matitaTypes.cmx: matitaTypes.cmi predefined_virtuals.cmo: virtuals.cmi predefined_virtuals.cmi @@ -69,7 +71,7 @@ matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmo \ matitaInit.cmi: matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi matitaMisc.cmi: matitaGuiTypes.cmi -matitaScript.cmi: matitaTypes.cmi +matitaScript.cmi: matitaTypes.cmi: predefined_virtuals.cmi: virtuals.cmi: diff --git a/matita/matita/.depend.opt b/matita/matita/.depend.opt index 42bbf72a0..ccf85d10f 100644 --- a/matita/matita/.depend.opt +++ b/matita/matita/.depend.opt @@ -30,14 +30,14 @@ matitaGui.cmx: virtuals.cmx matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi matitaInit.cmo: matitaExcPp.cmi buildTimeConf.cmx matitaInit.cmi matitaInit.cmx: matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi -matitaMathView.cmo: virtuals.cmi matitaTypes.cmi matitaScript.cmi \ - matitaMisc.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi \ - lablGraphviz.cmi cicMathView.cmi buildTimeConf.cmx \ - applyTransformation.cmi matitaMathView.cmi -matitaMathView.cmx: virtuals.cmx matitaTypes.cmx matitaScript.cmx \ - matitaMisc.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx \ - lablGraphviz.cmx cicMathView.cmx buildTimeConf.cmx \ - applyTransformation.cmx matitaMathView.cmi +matitaMathView.cmo: virtuals.cmi matitaTypes.cmi matitaMisc.cmi \ + matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi lablGraphviz.cmi \ + cicMathView.cmi buildTimeConf.cmx applyTransformation.cmi \ + matitaMathView.cmi +matitaMathView.cmx: virtuals.cmx matitaTypes.cmx matitaMisc.cmx \ + matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx lablGraphviz.cmx \ + cicMathView.cmx buildTimeConf.cmx applyTransformation.cmx \ + matitaMathView.cmi matitaMisc.cmo: matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi matitaMisc.cmx: matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi matita.cmo: predefined_virtuals.cmi matitaTypes.cmi matitaScript.cmi \ @@ -46,10 +46,12 @@ matita.cmo: predefined_virtuals.cmi matitaTypes.cmi matitaScript.cmi \ matita.cmx: predefined_virtuals.cmx matitaTypes.cmx matitaScript.cmx \ matitaMathView.cmx matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx \ buildTimeConf.cmx -matitaScript.cmo: virtuals.cmi matitaTypes.cmi matitaGtkMisc.cmi \ - matitaEngine.cmi cicMathView.cmi buildTimeConf.cmx matitaScript.cmi -matitaScript.cmx: virtuals.cmx matitaTypes.cmx matitaGtkMisc.cmx \ - matitaEngine.cmx cicMathView.cmx buildTimeConf.cmx matitaScript.cmi +matitaScript.cmo: virtuals.cmi matitaTypes.cmi matitaMathView.cmi \ + matitaGtkMisc.cmi matitaEngine.cmi cicMathView.cmi buildTimeConf.cmx \ + matitaScript.cmi +matitaScript.cmx: virtuals.cmx matitaTypes.cmx matitaMathView.cmx \ + matitaGtkMisc.cmx matitaEngine.cmx cicMathView.cmx buildTimeConf.cmx \ + matitaScript.cmi matitaTypes.cmo: matitaTypes.cmi matitaTypes.cmx: matitaTypes.cmi predefined_virtuals.cmo: virtuals.cmi predefined_virtuals.cmi @@ -69,7 +71,7 @@ matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmx \ matitaInit.cmi: matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi matitaMisc.cmi: matitaGuiTypes.cmi -matitaScript.cmi: matitaTypes.cmi +matitaScript.cmi: matitaTypes.cmi: predefined_virtuals.cmi: virtuals.cmi: diff --git a/matita/matita/Makefile b/matita/matita/Makefile index 2d1fae4bf..0271b714a 100644 --- a/matita/matita/Makefile +++ b/matita/matita/Makefile @@ -44,9 +44,9 @@ MLI = \ matitaGtkMisc.mli \ virtuals.mli \ cicMathView.mli \ - matitaScript.mli \ predefined_virtuals.mli \ matitaMathView.mli \ + matitaScript.mli \ matitaGui.mli \ $(NULL) CMLI = \ diff --git a/matita/matita/cicMathView.ml b/matita/matita/cicMathView.ml index f7e5b667a..ea7fd5160 100644 --- a/matita/matita/cicMathView.ml +++ b/matita/matita/cicMathView.ml @@ -30,8 +30,9 @@ open MatitaGtkMisc open MatitaGuiTypes open GtkSourceView2 -let matita_script_current = ref (fun _ -> assert false);; +let matita_script_current = ref (fun _ -> (assert false : < advance: ?statement:string -> unit -> unit; grafite_status: GrafiteTypes.status; setGoal: int option -> unit >));; let register_matita_script_current f = matita_script_current := f;; +let get_matita_script_current () = !matita_script_current ();; type document_element = string @@ -371,7 +372,7 @@ object (self) (GrafiteAst.Tactic (loc, Some (GrafiteAst.Reduce (loc, kind, pat)), GrafiteAst.Semicolon loc)) in - (!matita_script_current ())#advance ~statement () in + (get_matita_script_current ())#advance ~statement () in connect_menu_item copy gui#copy; connect_menu_item normalize (reduction_action `Normalize); connect_menu_item simplify (reduction_action `Simpl); @@ -506,7 +507,7 @@ object (self) else string_of_dom_node node method private string_of_cic_sequent ~output_type cic_sequent = - let script = !matita_script_current () in + let script = get_matita_script_current () in let metasenv = if script#onGoingProof () then script#proofMetasenv else [] in let map_unicode_to_tex = diff --git a/matita/matita/cicMathView.mli b/matita/matita/cicMathView.mli index 80e6bc886..bb95b3ef7 100644 --- a/matita/matita/cicMathView.mli +++ b/matita/matita/cicMathView.mli @@ -64,4 +64,7 @@ val screenshot: GrafiteTypes.status -> NCic.metasenv -> NCic.metasenv -> NCic.substitution -> string -> unit -val register_matita_script_current: (unit -> < advance: unit; onGoingProf: bool; metasenv: NCic.metasenv >) -> unit +(* CSC: these functions should completely disappear; bad design; + the object type is MatitaScript.script *) +val register_matita_script_current: (unit -> < advance: ?statement:string -> unit -> unit; grafite_status: GrafiteTypes.status; setGoal: int option -> unit >) -> unit +val get_matita_script_current: unit -> < advance: ?statement:string -> unit -> unit; grafite_status: GrafiteTypes.status; setGoal: int option -> unit > diff --git a/matita/matita/matita.ml b/matita/matita/matita.ml index 12cb9eeda..4b8548f19 100644 --- a/matita/matita/matita.ml +++ b/matita/matita/matita.ml @@ -50,7 +50,6 @@ let script = let s = MatitaScript.script ~source_view:gui#sourceView - ~mathviewer:(MatitaMathView.mathViewer ()) ~urichooser:(fun uris -> try MatitaGui.interactive_uri_choice ~selection_mode:`SINGLE diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index 4b5a9fc1d..ec536f60e 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -37,7 +37,7 @@ module Stack = Continuationals.Stack (** inherit from this class if you want to access current script *) class scriptAccessor = object (self) - method private script = MatitaScript.current () + method private script = get_matita_script_current () end let cicBrowsers = ref [] @@ -292,7 +292,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) let module Pp = GraphvizPp.Dot in let filename, oc = Filename.open_temp_file "matita" ".dot" in let fmt = Format.formatter_of_out_channel oc in - let status = (MatitaScript.current ())#grafite_status in + let status = (get_matita_script_current ())#grafite_status in Pp.header ~name:"Hints" ~graph_type:"graph" @@ -315,7 +315,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) ~name:"Coercions" ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"] ~edge_attrs:["fontsize", "10"] fmt; - let status = (MatitaScript.current ())#grafite_status in + let status = (get_matita_script_current ())#grafite_status in NCicCoercion.generate_dot_file status fmt; Pp.trailer fmt; Pp.raw "@." fmt; @@ -594,7 +594,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) method private _loadTermNCic term m s c = let d = 0 in let m = (0,([],c,term))::m in - let status = (MatitaScript.current ())#grafite_status in + let status = (get_matita_script_current ())#grafite_status in mathView#nload_sequent status m s d; self#_showMath @@ -690,19 +690,20 @@ let default_sequentsViewer () = sequentsViewer ~notebook:gui#main#sequentsNotebook ~cicMathView () let sequentsViewer_instance = MatitaMisc.singleton default_sequentsViewer -let mathViewer () = - object(self) - method private get_browser reuse = - if reuse then - (match !cicBrowsers with - | [] -> cicBrowser () - | b :: _ -> (b :> MatitaGuiTypes.cicBrowser)) - else - (cicBrowser ()) - method show_entry ?(reuse=false) t = (self#get_browser reuse)#load t - - end +(** @param reuse if set reused last opened cic browser otherwise +* opens a new one. default is false *) +let show_entry ?(reuse=false) t = + let browser = + if reuse then + (match !cicBrowsers with + [] -> cicBrowser () + | b :: _ -> (b :> MatitaGuiTypes.cicBrowser)) + else + cicBrowser () + in + browser#load t +;; let refresh_all_browsers () = List.iter (fun b -> b#refresh ~force:false ()) !cicBrowsers diff --git a/matita/matita/matitaMathView.mli b/matita/matita/matitaMathView.mli index 47b1e4a83..6cfd83eb3 100644 --- a/matita/matita/matitaMathView.mli +++ b/matita/matita/matitaMathView.mli @@ -28,14 +28,19 @@ val cicBrowser: unit -> MatitaGuiTypes.cicBrowser (** {2 Singleton instances} *) val sequentsViewer_instance: unit -> MatitaGuiTypes.sequentsViewer -val mathViewer: unit -> MatitaTypes.mathViewer (** {2 Global changes} *) val refresh_all_browsers: unit -> unit (** act on all cicBrowsers *) val update_font_sizes: unit -> unit - (** {3 Clipboard & Selection handling} *) +(** {2 Rendering in a browser} *) + +(** @param reuse if set reused last opened cic browser otherwise +* opens a new one. default is false *) +val show_entry: ?reuse:bool -> MatitaTypes.mathViewer_entry -> unit + +(** {2 Clipboard & Selection handling} *) val has_selection: unit -> bool diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index c50b4b571..02f9a23b0 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -66,7 +66,6 @@ let first_line s = with Not_found -> s type guistuff = { - mathviewer:MatitaTypes.mathViewer; urichooser: NReference.reference list -> NReference.reference list; ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL]; } @@ -132,7 +131,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us NotationPt.Cast (t,NotationPt.Implicit `JustOne)) (* XXX use the metasenv, if possible *) in - guistuff.mathviewer#show_entry (`NCic (t,ctx,m,s)); + MatitaMathView.show_entry (`NCic (t,ctx,m,s)); [status, parsed_text], "", parsed_text_length | TA.NIntroGuess _loc -> let names_ref = ref [] in @@ -247,7 +246,6 @@ let fresh_script_id = fun () -> incr i; !i class script ~(source_view: GSourceView2.source_view) - ~(mathviewer: MatitaTypes.mathViewer) ~set_star ~ask_confirmation ~urichooser @@ -287,7 +285,6 @@ object (self) val scriptId = fresh_script_id () val guistuff = { - mathviewer = mathviewer; urichooser = urichooser; ask_confirmation = ask_confirmation; } @@ -697,13 +694,14 @@ end let _script = ref None -let script ~source_view ~mathviewer ~urichooser ~ask_confirmation ~set_star () +let script ~source_view ~urichooser ~ask_confirmation ~set_star () = - let s = new script - ~source_view ~mathviewer ~ask_confirmation ~urichooser ~set_star () - in + let s = new script ~source_view ~ask_confirmation ~urichooser ~set_star () in _script := Some s; s let current () = match !_script with None -> assert false | Some s -> s +let _ = + CicMathView.register_matita_script_current (current :> unit -> < advance: ?statement:string -> unit -> unit; grafite_status: GrafiteTypes.status; setGoal: int option -> unit >) +;; diff --git a/matita/matita/matitaScript.mli b/matita/matita/matitaScript.mli index 50bc17eda..de95aac52 100644 --- a/matita/matita/matitaScript.mli +++ b/matita/matita/matitaScript.mli @@ -85,7 +85,6 @@ end * "*") on the side of a script name *) val script: source_view:GSourceView2.source_view -> - mathviewer: MatitaTypes.mathViewer-> urichooser: (NReference.reference list -> NReference.reference list) -> ask_confirmation: (title:string -> message:string -> [`YES | `NO | `CANCEL]) -> diff --git a/matita/matita/matitaTypes.ml b/matita/matita/matitaTypes.ml index 6ead6da47..a772ae946 100644 --- a/matita/matita/matitaTypes.ml +++ b/matita/matita/matitaTypes.ml @@ -75,11 +75,3 @@ let entry_of_string = function | "about:grammar" -> `About `Grammar | _ -> (* only about entries supported ATM *) raise (Invalid_argument "entry_of_string") - -class type mathViewer = - object - (** @param reuse if set reused last opened cic browser otherwise - * opens a new one. default is false - *) - method show_entry: ?reuse:bool -> mathViewer_entry -> unit - end diff --git a/matita/matita/matitaTypes.mli b/matita/matita/matitaTypes.mli index 651294e96..75fca5049 100644 --- a/matita/matita/matitaTypes.mli +++ b/matita/matita/matitaTypes.mli @@ -38,8 +38,3 @@ type mathViewer_entry = val string_of_entry : mathViewer_entry -> string val entry_of_string : string -> mathViewer_entry - -class type mathViewer = - object - method show_entry : ?reuse:bool -> mathViewer_entry -> unit - end -- 2.39.2