- hExtlib: added debugging information for split_nth

[helm.git] / helm / software / matita / matitaMathView.ml

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index f57dc4d320824cd2e67fb213a5368c5dd596c16a..9c259a1cbdc58297d902974a20b8caa77014e8e5 100644 (file)
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -593,6 +593,19 @@ object (self)
     end;
     self#load_root ~root:mathml#get_documentElement
 
+  method nload_sequent metasenv subst metano =
+    let sequent = List.assoc metano metasenv in
+    let mathml =
+     ApplyTransformation.nmml_of_cic_sequent metasenv subst (metano,sequent)
+    in
+    if BuildTimeConf.debug then begin
+      let name =
+       "/tmp/sequent_viewer_" ^ string_of_int (Unix.getuid ()) ^ ".xml" in
+      HLog.debug ("load_sequent: dumping MathML to ./" ^ name);
+      ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ())
+    end;
+    self#load_root ~root:mathml#get_documentElement
+
   method load_object obj =
     let use_diff = false in (* ZACK TODO use XmlDiff when re-rendering? *)
     let (mathml,
@@ -642,7 +655,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
     val mutable page2goal = []  (* associative list: page no -> goal no *)
     val mutable goal2page = []  (* the other way round *)
     val mutable goal2win = []   (* associative list: goal no -> scrolled win *)
-    val mutable _metasenv = []
+    val mutable _metasenv = `Old []
     val mutable scrolledWin: GBin.scrolled_window option = None
       (* scrolled window to which the sequentViewer is currently attached *)
     val logo = (GMisc.image
@@ -681,13 +694,13 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
       page2goal <- [];
       goal2page <- [];
       goal2win <- [];
-      _metasenv <- []; 
+      _metasenv <- `Old []; 
       self#script#setGoal None
 
     method load_sequents 
       { proof = (_,metasenv,_subst,_,_, _) as proof; stack = stack } 
     =
-      _metasenv <- metasenv;
+      _metasenv <- `Old metasenv;
       pages <- 0;
       let win goal_switch =
         let w =
@@ -764,9 +777,92 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
           self#script#setGoal (Some (goal_of_switch goal_switch));
           self#render_page ~page ~goal_switch))
 
+    method nload_sequents 
+      { NTacStatus.istatus = { NTacStatus.pstatus = (_,_,metasenv,subst,_) }; gstatus = stack } 
+    =
+      _metasenv <- `New (metasenv,subst);
+      pages <- 0;
+      let win goal_switch =
+        let w =
+          GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`ALWAYS
+            ~shadow_type:`IN ~show:true ()
+        in
+        let reparent () =
+          scrolledWin <- Some w;
+          match cicMathView#misc#parent with
+          | None -> w#add cicMathView#coerce
+          | Some parent ->
+             let parent =
+              match cicMathView#misc#parent with
+                 None -> assert false
+               | Some p -> GContainer.cast_container p
+             in
+              parent#remove cicMathView#coerce;
+              w#add cicMathView#coerce
+        in
+        goal2win <- (goal_switch, reparent) :: goal2win;
+        w#coerce
+      in
+      assert (
+        let stack_goals = Stack.open_goals stack in
+        let proof_goals = List.map fst metasenv in
+        if
+          HExtlib.list_uniq (List.sort Pervasives.compare stack_goals)
+          <> List.sort Pervasives.compare proof_goals
+        then begin
+          prerr_endline ("STACK GOALS = " ^ String.concat " " (List.map string_of_int stack_goals));
+          prerr_endline ("PROOF GOALS = " ^ String.concat " " (List.map string_of_int proof_goals));
+          false
+        end
+        else true
+      );
+      let render_switch =
+        function Stack.Open i ->`Meta i | Stack.Closed i ->`Closed (`Meta i)
+      in
+      let page = ref 0 in
+      let added_goals = ref [] in
+        (* goals can be duplicated on the tack due to focus, but we should avoid
+         * multiple labels in the user interface *)
+      let add_tab markup goal_switch =
+        let goal = Stack.goal_of_switch goal_switch in
+        if not (List.mem goal !added_goals) then begin
+          ignore(notebook#append_page 
+            ~tab_label:(tab_label markup) (win goal_switch));
+          page2goal <- (!page, goal_switch) :: page2goal;
+          goal2page <- (goal_switch, !page) :: goal2page;
+          incr page;
+          pages <- pages + 1;
+          added_goals := goal :: !added_goals
+        end
+      in
+      let add_switch _ _ (_, sw) = add_tab (render_switch sw) sw in
+      Stack.iter  (** populate notebook with tabs *)
+        ~env:(fun depth tag (pos, sw) ->
+          let markup =
+            match depth, pos with
+            | 0, 0 -> `Current (render_switch sw)
+            | 0, _ -> `Shift (pos, `Current (render_switch sw))
+            | 1, pos when Stack.head_tag stack = `BranchTag ->
+                `Shift (pos, render_switch sw)
+            | _ -> render_switch sw
+          in
+          add_tab markup sw)
+        ~cont:add_switch ~todo:add_switch
+        stack;
+      switch_page_callback <-
+        Some (notebook#connect#switch_page ~callback:(fun page ->
+          let goal_switch =
+            try List.assoc page page2goal with Not_found -> assert false
+          in
+          self#script#setGoal (Some (goal_of_switch goal_switch));
+          self#render_page ~page ~goal_switch))
+
     method private render_page ~page ~goal_switch =
       (match goal_switch with
-      | Stack.Open goal -> cicMathView#load_sequent _metasenv goal
+      | Stack.Open goal ->
+         (match _metasenv with
+             `Old menv -> cicMathView#load_sequent menv goal
+           | `New (menv,subst) -> cicMathView#nload_sequent menv subst goal)
       | Stack.Closed goal ->
           let doc = Lazy.force closed_goal_mathml in
           cicMathView#load_root ~root:doc#get_documentElement);