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.

diff --git a/matita/matita/.depend b/matita/matita/.depend
index d7b9a80a15c8c44746b6d0c12f4a7f31a049d068..0d51469a61f12e4d581869abb386368005e20ae7 100644 (file)
--- 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 42bbf72a0f4ab6ed404f24305a0329261c8150db..ccf85d10f8edf47ba5f6ba53b47733624bceb98a 100644 (file)
--- 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 2d1fae4bf6fc2b0ad4ed3633a2a9c57cfa96cb8f..0271b714a5566704a599af382be964fb34532b89 100644 (file)
--- 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 f7e5b667afae50ef0cc2bbeae10adcecb1a38f84..ea7fd5160ee58e1821f5e92770f644f51c44530e 100644 (file)
--- 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 80e6bc8862407dd944001b2704129c1344ce7b78..bb95b3ef7f256ea4fd3b6ccac46fc786af1c407a 100644 (file)
--- 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 12cb9eedafac1e7a96d11e68d7711b41146603d8..4b8548f1932386d13f024f2f82e5789479b0409b 100644 (file)
--- 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 4b5a9fc1dd0ab4be0e710ce119b3c9898f898dec..ec536f60ef6ea5b03beb74121ed2cc8eb07ba24b 100644 (file)
--- 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 47b1e4a83eb6584762ae715fdae0e847ebab43db..6cfd83eb3094bcf513878e9038bf0b13ecbc3699 100644 (file)
--- 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 c50b4b5716e20a468980147931a6e6fbe0f28b05..02f9a23b00ad504106b65387763e31361a56f5cd 100644 (file)
--- 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 50bc17eda08991223f1b74d108c21218c3e9040f..de95aac52ce9618500c05f5ed030aa5292a01843 100644 (file)
--- 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 6ead6da4769eb85c1444ee560a4af08dbb73b1bd..a772ae94695933f7a27fd20ae50783936074ec6b 100644 (file)
--- 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 651294e964ff00c0b9113651765b85b62262b1a9..75fca5049a650621a0f98a9ba8b515275e4172fa 100644 (file)
--- 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