X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=1ad4b2cd10a79dd14348b67d157d4b4b7552beab;hb=9b193e984a2ab8c94e4c032c382f17c6c436938d;hp=be144b9492f9ef9cd5d36cf49948799da445aaf3;hpb=25992baa7fb25b39694f138b8d1483a249b1a266;p=helm.git

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index be144b949..1ad4b2cd1 100644
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -28,10 +28,12 @@ open Printf
 open MatitaTypes
 open MatitaGtkMisc
 
+module Stack = Continuationals.Stack
+
 (** inherit from this class if you want to access current script *)
 class scriptAccessor =
 object (self)
-  method private script = MatitaScript.instance ()
+  method private script = MatitaScript.current ()
 end
 
 let cicBrowsers = ref []
@@ -284,7 +286,7 @@ object (self)
       List.hd (HExtlib.split ~sep:' ' xref_attr#to_string)
     in
     let id = get_id node in
-    let script = MatitaScript.instance () in
+    let script = MatitaScript.current () in
     let metasenv = script#proofMetasenv in
     let context = script#proofContext in
     let metasenv, context, conclusion =
@@ -363,7 +365,8 @@ object (self)
       ApplyTransformation.mml_of_cic_sequent metasenv sequent
     in
     self#set_cic_info
-      (Some (ids_to_terms, ids_to_hypotheses, ids_to_father_ids, Hashtbl.create 1, None));
+      (Some (ids_to_terms, ids_to_hypotheses, ids_to_father_ids,
+        Hashtbl.create 1, None));
     let name = "sequent_viewer.xml" in
     MatitaLog.debug ("load_sequent: dumping MathML to ./" ^ name);
     ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ());
@@ -391,6 +394,19 @@ object (self)
         current_mathml <- Some mathml);
 end
 
+let tab_label meta_markup =
+  let rec aux =
+    function
+    | `Current m -> sprintf "<b>%s</b>" (aux m)
+    | `Closed m -> sprintf "<s>%s</s>" (aux m)
+    | `Shift (pos, m) -> sprintf "|<sub>%d</sub>: %s" pos (aux m)
+    | `Meta n -> sprintf "?%d" n
+  in
+  let markup = aux meta_markup in
+  (GMisc.label ~markup ~show:true ())#coerce
+
+let goal_of_switch = function Stack.Open g | Stack.Closed g -> g
+
 class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
   object (self)
     inherit scriptAccessor
@@ -419,9 +435,6 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
      notebook#set_show_tabs false;
      notebook#append_page logo_with_qed
 
-    method private tab_label metano =
-      (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce
-
     method reset =
       (match scrolledWin with
       | Some w ->
@@ -444,13 +457,11 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
       _metasenv <- []; 
       self#script#setGoal ~-1;
 
-    method load_sequents (status: ProofEngineTypes.status) =
-      let ((_, metasenv, _, _), goal) = status in
+    method load_sequents { proof = (_,metasenv,_,_) as proof; stack = stack } =
       let sequents_no = List.length metasenv in
       _metasenv <- metasenv;
-      pages <- sequents_no;
-      self#script#setGoal goal;
-      let win metano =
+      pages <- 0;
+      let win goal_switch =
         let w =
           GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`ALWAYS
             ~shadow_type:`IN ~show:true ()
@@ -468,42 +479,82 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
               parent#remove cicMathView#coerce;
               w#add cicMathView#coerce
         in
-        goal2win <- (metano, reparent) :: goal2win;
+        goal2win <- (goal_switch, reparent) :: goal2win;
         w#coerce
       in
+      assert (
+        let stack_goals = Stack.open_goals stack in
+        let proof_goals = ProofEngineTypes.goals_of_proof proof 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
-      List.iter
-        (fun (metano, _, _) ->
-          page2goal <- (!page, metano) :: page2goal;
-          goal2page <- (metano, !page) :: goal2page;
+      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
+          notebook#append_page ~tab_label:(tab_label markup) (win goal_switch);
+          page2goal <- (!page, goal_switch) :: page2goal;
+          goal2page <- (goal_switch, !page) :: goal2page;
           incr page;
-          notebook#append_page ~tab_label:(self#tab_label metano) (win metano))
-        metasenv;
+          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, _ -> `Current (render_switch sw)
+            | 1, pos when Stack.head_tag stack = 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 =
-            try
-              List.assoc page page2goal
-            with Not_found -> assert false
+          let goal_switch =
+            try List.assoc page page2goal with Not_found -> assert false
           in
-          self#script#setGoal goal;
-          self#render_page ~page ~goal))
-
-    method private render_page ~page ~goal =
-      cicMathView#load_sequent _metasenv goal;
-      try
-        List.assoc goal goal2win ();
-        cicMathView#set_selection None
-      with Not_found -> assert false
+          self#script#setGoal (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.Closed goal ->
+          let doc = Lazy.force MatitaMisc.closed_goal_mathml in
+          cicMathView#load_root ~root:doc#get_documentElement);
+      (try
+        cicMathView#set_selection None;
+        List.assoc goal_switch goal2win ()
+      with Not_found -> assert false)
 
     method goto_sequent goal =
-      let page =
+      let goal_switch, page =
         try
-          List.assoc goal goal2page
+          List.find
+            (function Stack.Open g, _ | Stack.Closed g, _ -> g = goal)
+            goal2page
         with Not_found -> assert false
       in
       notebook#goto_page page;
-      self#render_page page goal
+      self#render_page page goal_switch
 
   end
 
@@ -591,7 +642,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     try
       f ()
     with exn ->
-      if Helm_registry.get_bool "matita.catch_top_level_exn" then
+      if not (Helm_registry.get_bool "matita.debug") then
         fail (MatitaExcPp.to_string exn)
       else raise exn
   in
@@ -611,7 +662,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
         let query = String.lowercase (List.nth queries combo#active) in
         let input = win#queryInputText#text in
         let statement = "whelp " ^ query ^ " " ^ input ^ "." in
-        (MatitaScript.instance ())#advance ~statement ()
+        (MatitaScript.current ())#advance ~statement ()
       in
       ignore(win#queryInputText#connect#activate ~callback:start_query);
       ignore(combo#connect#changed ~callback:start_query);
@@ -724,7 +775,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
 
     method private blank () =
       self#_showMath;
-      mathView#load_root (MatitaMisc.empty_mathml ())#get_documentElement
+      mathView#load_root
+        (Lazy.force MatitaMisc.empty_mathml)#get_documentElement
 
     method private _loadCheck term =
       failwith "not implemented _loadCheck";
@@ -741,7 +793,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           let name = UriManager.name_of_uri (HExtlib.unopt uri) in
           let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
           self#_loadObj obj
-      | Incomplete_proof ((uri, metasenv, bo, ty), _) -> 
+      | Incomplete_proof { proof = (uri, metasenv, bo, ty) } ->
           let name = UriManager.name_of_uri (HExtlib.unopt uri) in
           let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
           self#_loadObj obj
@@ -805,7 +857,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       in
       if is_whelp txt then begin
         set_whelp_query txt;  
-        (MatitaScript.instance ())#advance ~statement:(txt ^ ".") ()
+        (MatitaScript.current ())#advance ~statement:(txt ^ ".") ()
       end else begin
         let entry =
           match txt with
@@ -834,7 +886,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
 
   end
   
-let sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
+let sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) ():
+  MatitaGuiTypes.sequentsViewer
+=
   new sequentsViewer ~notebook ~cicMathView ()
 
 let cicBrowser () =
@@ -897,7 +951,7 @@ let get_math_views () =
   :: (List.map (fun b -> b#mathView) !cicBrowsers)
 
 let get_selections () =
-  if (MatitaScript.instance ())#onGoingProof () then
+  if (MatitaScript.current ())#onGoingProof () then
     let rec aux =
       function
       | [] -> None