X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=794b849c4918202171780c1b2c496c0b1b7a7a2e;hb=aa0d60227b785da3355b31519ba11cb4fbd2c925;hp=4297634c809e423c8856efb4c24d7ff7384973ad;hpb=86af949158e013178557c7fec7662ac06fae753c;p=helm.git

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 4297634c8..794b849c4 100644
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -23,15 +23,20 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* $Id$ *)
+
 open Printf
 
-open MatitaTypes
+open GrafiteTypes
 open MatitaGtkMisc
+open MatitaGuiTypes
+
+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 []
@@ -60,9 +65,27 @@ let near (x1, y1) (x2, y2) =
   let distance = sqrt (((x2 -. x1) ** 2.) +. ((y2 -. y1) ** 2.)) in
   (distance < 4.)
 
+let xlink_ns = Gdome.domString "http://www.w3.org/1999/xlink"
+let helm_ns = Gdome.domString "http://www.cs.unibo.it/helm"
 let href_ds = Gdome.domString "href"
 let xref_ds = Gdome.domString "xref"
 
+let domImpl = Gdome.domImplementation ()
+
+  (** Gdome.element of a MathML document whose rendering should be blank. Used
+  * by cicBrowser to render "about:blank" document *)
+let empty_mathml = lazy (
+  domImpl#createDocument ~namespaceURI:(Some DomMisc.mathml_ns)
+    ~qualifiedName:(Gdome.domString "math") ~doctype:None)
+
+let empty_boxml = lazy (
+  domImpl#createDocument ~namespaceURI:(Some DomMisc.boxml_ns) 
+    ~qualifiedName:(Gdome.domString "box") ~doctype:None)
+
+  (** shown for goals closed by side effects *)
+let closed_goal_mathml = lazy (
+  domImpl#createDocumentFromURI ~uri:BuildTimeConf.closed_xml ())
+
 (* ids_to_terms should not be passed here, is just for debugging *)
 let find_root_id annobj id ids_to_father_ids ids_to_terms ids_to_inner_types =
   let find_parent id ids =
@@ -116,8 +139,24 @@ let string_of_dom_node node =
         text#get_data#to_string
       with GdomeInit.DOMCastException _ -> "")
 
+let name_of_hypothesis = function
+  | Some (Cic.Name s, _) -> s
+  | _ -> assert false
+
+let id_of_node (node: Gdome.element) =
+  let xref_attr =
+    node#getAttributeNS ~namespaceURI:helm_ns ~localName:xref_ds in
+  try
+    List.hd (HExtlib.split ~sep:' ' xref_attr#to_string)
+  with Failure _ -> assert false
+
+type selected_term =
+  | SelTerm of Cic.term * string option (* term, parent hypothesis (if any) *)
+  | SelHyp of string * Cic.context (* hypothesis, context *)
+
 class clickableMathView obj =
 let text_width = 80 in
+let dummy_loc = HExtlib.dummy_floc in
 object (self)
   inherit GMathViewAux.multi_selection_math_view obj
 
@@ -141,12 +180,23 @@ object (self)
   val mutable selection_changed = false
 
   method private selection_get_cb ctxt ~info ~time =
-    (match self#get_selections with
-    | [] -> ()
-    | node :: _ -> ctxt#return (self#string_of_node node))
+    let text =
+      match ctxt#target with
+      | "PATTERN" -> self#text_of_selection `Pattern
+      | "TERM" | _ -> self#text_of_selection `Term
+    in
+    match text with
+    | None -> ()
+    | Some s -> ctxt#return s
+
+  method private text_of_selection fmt =
+    match self#get_selections with
+    | [] -> None
+    | node :: _ -> Some (self#string_of_node ~paste_kind:fmt node)
 
   method private selection_clear_cb sel_event =
     self#remove_selections;
+    (GData.clipboard Gdk.Atom.clipboard)#clear ();
     false
 
   method private button_press_cb gdk_button =
@@ -159,21 +209,59 @@ object (self)
       self#popup_contextual_menu (GdkEvent.Button.time gdk_button);
     false
 
+    (** @return a pattern structure which contains pretty printed terms *)
+  method private tactic_text_pattern_of_selection =
+    match self#get_selections with
+    | [] -> assert false (* this method is invoked only if there's a sel. *)
+    | node :: _ ->
+        let id = id_of_node node in
+        let cic_info, unsh_sequent = self#get_cic_info id in
+        match self#get_term_by_id cic_info id with
+        | SelTerm (t, father_hyp) ->
+            let sequent = self#sequent_of_id ~paste_kind:`Pattern id in
+            let text = self#string_of_cic_sequent sequent in
+            (match father_hyp with
+            | None -> None, [], Some text
+            | Some hyp_name -> None, [ hyp_name, text ], None)
+        | SelHyp (hyp_name, _ctxt) -> None, [ hyp_name, "%" ], None
+
   method private popup_contextual_menu time =
-    match self#string_of_selection with
-    | None -> ()
-    | Some s ->
-        let clipboard = GData.clipboard Gdk.Atom.clipboard in
-        let menu = GMenu.menu () in
-        let copy_menu_item =
-          GMenu.image_menu_item
-            ~label:"_Copy" ~stock:`COPY ~packing:menu#append ()
-        in
-        connect_menu_item copy_menu_item (fun () -> clipboard#set_text s);
-        menu#popup ~button:right_button ~time
+    let menu = GMenu.menu () in
+    let add_menu_item ?(menu = menu) ?stock ?label () =
+      GMenu.image_menu_item ?stock ?label ~packing:menu#append () in
+    let check = add_menu_item ~label:"Check" () in
+    let reductions_menu_item = GMenu.menu_item ~label:"βδιζ-reduce" () in
+    menu#append reductions_menu_item;
+    let reductions = GMenu.menu () in
+    reductions_menu_item#set_submenu reductions;
+    let normalize = add_menu_item ~menu:reductions ~label:"Normalize" () in
+    let reduce = add_menu_item ~menu:reductions ~label:"Reduce" () in
+    let simplify = add_menu_item ~menu:reductions ~label:"Simplify" () in
+    let whd = add_menu_item ~menu:reductions ~label:"Weak head" () in
+    menu#append (GMenu.separator_item ());
+    let copy = add_menu_item ~stock:`COPY () in
+    let gui = get_gui () in
+    List.iter (fun item -> item#misc#set_sensitive gui#canCopy)
+      [ copy; check; normalize; reduce; simplify; whd ];
+    let reduction_action kind () =
+      let pat = self#tactic_text_pattern_of_selection in
+      let statement =
+        let loc = HExtlib.dummy_floc in
+        "\n" ^
+        GrafiteAstPp.pp_executable ~term_pp:(fun s -> s)
+          ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false)
+          (GrafiteAst.Tactical (loc,
+            GrafiteAst.Tactic (loc, GrafiteAst.Reduce (loc, kind, pat)),
+            Some (GrafiteAst.Semicolon loc))) in
+      (MatitaScript.current ())#advance ~statement () in
+    connect_menu_item copy gui#copy;
+    connect_menu_item normalize (reduction_action `Normalize);
+    connect_menu_item reduce (reduction_action `Reduce);
+    connect_menu_item simplify (reduction_action `Simpl);
+    connect_menu_item whd (reduction_action `Whd);
+    menu#popup ~button:right_button ~time
 
   method private button_release_cb gdk_button =
-    let clipboard = GData.clipboard Gdk.Atom.primary in
     if GdkEvent.Button.button gdk_button = left_button then begin
       let button_release_x = GdkEvent.Button.x gdk_button in
       let button_release_y = GdkEvent.Button.y gdk_button in
@@ -188,11 +276,11 @@ object (self)
           (match self#get_element_at x y with
           | None -> ()
           | Some elt ->
-              let namespaceURI = DomMisc.xlink_ns in
               let localName = href_ds in
-              if elt#hasAttributeNS ~namespaceURI ~localName then
+              if elt#hasAttributeNS ~namespaceURI:xlink_ns ~localName then
                 self#invoke_href_callback
-                  (elt#getAttributeNS ~namespaceURI ~localName)#to_string
+                  (elt#getAttributeNS ~namespaceURI:xlink_ns
+                    ~localName)#to_string
                   gdk_button
               else
                 ignore (self#action_toggle elt));
@@ -213,23 +301,20 @@ object (self)
               List.iter
                 (fun uri ->
                   let menu_item =
-                    GMenu.menu_item ~label:uri ~packing:menu#append ()
-                  in
+                    GMenu.menu_item ~label:uri ~packing:menu#append () in
                   connect_menu_item menu_item (fun () -> f uri))
                 uris;
               menu#popup ~button ~time)
 
   method private choose_selection_cb gdome_elt =
-    let (gui: MatitaGuiTypes.gui) = get_gui () in
-    let clipboard = GData.clipboard Gdk.Atom.primary in
     let set_selection elt =
+      let misc = self#coerce#misc in
       self#set_selection (Some elt);
-      self#coerce#misc#add_selection_target
-        ~target:(Gdk.Atom.name Gdk.Atom.string) Gdk.Atom.primary;
-      ignore (self#coerce#misc#grab_selection Gdk.Atom.primary)
+      misc#add_selection_target ~target:"STRING" Gdk.Atom.primary;
+      ignore (misc#grab_selection Gdk.Atom.primary);
     in
     let rec aux elt =
-      if (elt#getAttributeNS ~namespaceURI:DomMisc.helm_ns
+      if (elt#getAttributeNS ~namespaceURI:helm_ns
             ~localName:xref_ds)#to_string <> ""
       then
         set_selection elt
@@ -241,7 +326,7 @@ object (self)
         with GdomeInit.DOMCastException _ -> ()
     in
     (match gdome_elt with
-    | Some elt when (elt#getAttributeNS ~namespaceURI:DomMisc.xlink_ns
+    | Some elt when (elt#getAttributeNS ~namespaceURI:xlink_ns
         ~localName:href_ds)#to_string <> "" ->
           set_selection elt
     | Some elt -> aux elt
@@ -250,96 +335,134 @@ object (self)
 
   method update_font_size = self#set_font_size !current_font_size
 
-  method private get_term_by_id context cic_info id =
-    let ids_to_terms, ids_to_hypotheses, _, _, _ = cic_info in
+    (** find a term by id from stored CIC infos @return either `Hyp if the id
+     * correspond to an hypothesis or `Term (cic, hyp) if the id correspond to a
+     * term. In the latter case hyp is either None (if the term is a subterm of
+     * the sequent conclusion) or Some hyp_name if the term belongs to an
+     * hypothesis *)
+  method private get_term_by_id cic_info id =
+    let unsh_item, ids_to_terms, ids_to_hypotheses, ids_to_father_ids, _, _ =
+      cic_info in
+    let rec find_father_hyp id =
+      if Hashtbl.mem ids_to_hypotheses id
+      then Some (name_of_hypothesis (Hashtbl.find ids_to_hypotheses id))
+      else
+        let father_id =
+          try Hashtbl.find ids_to_father_ids id
+          with Not_found -> assert false in
+        match father_id with
+        | Some id -> find_father_hyp id
+        | None -> None
+    in
     try
-      `Term (Hashtbl.find ids_to_terms id)
+      let term = Hashtbl.find ids_to_terms id in
+      let father_hyp = find_father_hyp id in
+      SelTerm (term, father_hyp)
     with Not_found ->
       try
         let hyp = Hashtbl.find ids_to_hypotheses id in
+        let _, context, _ =
+          match unsh_item with Some seq -> seq | None -> assert false in
         let context' = MatitaMisc.list_tl_at hyp context in
-        `Hyp context'
+        SelHyp (name_of_hypothesis hyp, context')
       with Not_found -> assert false
     
   method private find_obj_conclusion id =
     match self#cic_info with
     | None
-    | Some (_, _, _, _, None) -> assert false
-    | Some (ids_to_terms, _, ids_to_father_ids, ids_to_inner_types, Some annobj) ->
+    | Some (_, _, _, _, _, None) -> assert false
+    | Some (_, ids_to_terms, _, ids_to_father_ids, ids_to_inner_types, Some annobj) ->
         let id =
          find_root_id annobj id ids_to_father_ids ids_to_terms ids_to_inner_types
         in
          (try Hashtbl.find ids_to_terms id with Not_found -> assert false)
 
-  method private string_of_node node =
-    if node#hasAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds
-    then self#string_of_id_node node
+  method private string_of_node ~(paste_kind:paste_kind) node =
+    if node#hasAttributeNS ~namespaceURI:helm_ns ~localName:xref_ds
+    then
+      let id = id_of_node node in
+      self#string_of_cic_sequent (self#sequent_of_id ~paste_kind id)
     else string_of_dom_node node
 
-  method private string_of_id_node node =
-    let get_id (node: Gdome.element) =
-      let xref_attr =
-        node#getAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds
-      in
-      xref_attr#to_string
-    in
-    let id = get_id node in
-    let script = MatitaScript.instance () in
-    let metasenv = script#proofMetasenv in
-    let context = script#proofContext in
-    let metasenv, context, conclusion =
-      if script#onGoingProof () then
-        script#proofMetasenv, script#proofContext, script#proofConclusion
-      else
-        [], [],
+  method private string_of_cic_sequent cic_sequent =
+    let script = MatitaScript.current () in
+    let metasenv =
+      if script#onGoingProof () then script#proofMetasenv else [] in
+    let _, (acic_sequent, _, _, ids_to_inner_sorts, _) =
+      Cic2acic.asequent_of_sequent metasenv cic_sequent in
+    let _, _, _, annterm = acic_sequent in
+    let ast, ids_to_uris =
+      TermAcicContent.ast_of_acic ids_to_inner_sorts annterm in
+    let pped_ast = TermContentPres.pp_ast ast in
+    let markup = CicNotationPres.render ids_to_uris pped_ast in
+    BoxPp.render_to_string text_width markup
+
+  method private pattern_of term context unsh_sequent =
+    let context_len = List.length context in
+    let _, unsh_context, conclusion = unsh_sequent in
+    try
+      (match
+        List.nth unsh_context (List.length unsh_context - context_len - 1)
+      with
+      | None -> assert false (* can't select a restricted hypothesis *)
+      | Some (name, Cic.Decl ty) ->
+          ProofEngineHelpers.pattern_of ~term:ty [term]
+      | Some (name, Cic.Def (bo, _)) ->
+          ProofEngineHelpers.pattern_of ~term:bo [term])
+    with Failure _ | Invalid_argument _ ->
+      ProofEngineHelpers.pattern_of ~term:conclusion [term]
+
+  method private get_cic_info id =
+    match self#cic_info with
+    | Some ((Some unsh_sequent, _, _, _, _, _) as info) -> info, unsh_sequent
+    | Some ((None, _, _, _, _, _) as info) ->
         let t = self#find_obj_conclusion id in
-        MatitaLog.debug (CicPp.ppterm t);
-        t
-    in
-(* TODO: code for patterns
-    let conclusion = (MatitaScript.instance ())#proofConclusion in
-    let conclusion_pattern =
-      ProofEngineHelpers.pattern_of ~term:conclusion cic_terms
-    in
-*)
-    let string_of_cic_sequent cic_sequent =
-      let acic_sequent, _, _, ids_to_inner_sorts, _ =
-        Cic2acic.asequent_of_sequent metasenv cic_sequent
-      in
-      let _, _, _, annterm = acic_sequent in
-      let ast, ids_to_uris =
-        CicNotationRew.ast_of_acic ids_to_inner_sorts annterm
-      in
-      let pped_ast = CicNotationRew.pp_ast ast in
-      let markup = CicNotationPres.render ids_to_uris pped_ast in
-      BoxPp.render_to_string text_width markup
-    in
-    let cic_info =
-      match self#cic_info with Some info -> info | None -> assert false
-    in
-    let cic_sequent =
-      match self#get_term_by_id context cic_info id with
-      | `Term t ->
-          let context' =
-            match
-              ProofEngineHelpers.locate_in_conjecture t
-                (~-1, context, conclusion)
-            with
-              [context,_] -> context
-            | _ -> assert false (* since it uses physical equality *)
-          in
-          ~-1, context', t
-      | `Hyp context -> ~-1, context, Cic.Rel 1
-    in
-    string_of_cic_sequent cic_sequent
-
-  method string_of_selections =
-    List.map self#string_of_node (List.rev self#get_selections)
+        info, (~-1, [], t) (* dummy sequent for obj *)
+    | None -> assert false
 
-  method string_of_selection =
+  method private sequent_of_id ~(paste_kind:paste_kind) id =
+    let cic_info, unsh_sequent = self#get_cic_info id in
+    let cic_sequent =
+      match self#get_term_by_id cic_info id with
+      | SelTerm (t, _father_hyp) ->
+          let occurrences =
+            ProofEngineHelpers.locate_in_conjecture t unsh_sequent in
+          (match occurrences with
+          | [ context, _t ] ->
+              (match paste_kind with
+              | `Term -> ~-1, context, t
+              | `Pattern -> ~-1, [], self#pattern_of t context unsh_sequent)
+          | _ ->
+              HLog.error (sprintf "found %d occurrences while 1 was expected"
+                (List.length occurrences));
+              assert false) (* since it uses physical equality *)
+      | SelHyp (_name, context) -> ~-1, context, Cic.Rel 1 in
+    cic_sequent
+
+  method private string_of_selection ~(paste_kind:paste_kind) =
     match self#get_selections with
     | [] -> None
-    | node :: _ -> Some (self#string_of_node node)
+    | node :: _ -> Some (self#string_of_node ~paste_kind node)
+
+  method has_selection = self#get_selections <> []
+
+    (** @return an associative list format -> string with all possible selection
+     * formats. Rationale: in order to convert the selection to TERM or PATTERN
+     * format we need the sequent, the metasenv, ... keeping all of them in a
+     * closure would be more expensive than keeping their already converted
+     * forms *)
+  method strings_of_selection =
+    try
+      let misc = self#coerce#misc in
+      List.iter
+        (fun target -> misc#add_selection_target ~target Gdk.Atom.clipboard)
+        [ "TERM"; "PATTERN"; "STRING" ];
+      ignore (misc#grab_selection Gdk.Atom.clipboard);
+      List.map
+        (fun paste_kind ->
+          paste_kind, HExtlib.unopt (self#string_of_selection ~paste_kind))
+        [ `Term; `Pattern ]
+    with Failure _ -> failwith "no selection"
 
 end
 
@@ -359,14 +482,18 @@ object (self)
 
   method load_sequent metasenv metano =
     let sequent = CicUtil.lookup_meta metano metasenv in
-    let (mathml, (_, (ids_to_terms, ids_to_father_ids, ids_to_hypotheses,_ ))) =
+    let (mathml, unsh_sequent,
+      (_, (ids_to_terms, ids_to_father_ids, ids_to_hypotheses,_ )))
+    =
       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 (Some unsh_sequent,
+        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 ());
+    HLog.debug ("load_sequent: dumping MathML to ./" ^ name);
+    ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ());
     self#load_root ~root:mathml#get_documentElement
 
   method load_object obj =
@@ -377,7 +504,7 @@ object (self)
       ApplyTransformation.mml_of_cic_object obj
     in
     self#set_cic_info
-      (Some (ids_to_terms, ids_to_hypotheses, ids_to_father_ids, ids_to_inner_types, Some annobj));
+      (Some (None, ids_to_terms, ids_to_hypotheses, ids_to_father_ids, ids_to_inner_types, Some annobj));
     (match current_mathml with
     | Some current_mathml when use_diff ->
         self#freeze;
@@ -385,12 +512,25 @@ object (self)
         self#thaw
     |  _ ->
         let name = "cic_browser.xml" in
-        MatitaLog.debug ("cic_browser: dumping MathML to ./" ^ name);
-        ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ());
+        HLog.debug ("cic_browser: dumping MathML to ./" ^ name);
+        ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ());
         self#load_root ~root:mathml#get_documentElement;
         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,10 +559,8 @@ 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 =
+      cicMathView#remove_selections;
       (match scrolledWin with
       | Some w ->
           (* removing page from the notebook will destroy all contained widget,
@@ -444,13 +582,10 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
       _metasenv <- []; 
       self#script#setGoal ~-1;
 
-    method load_sequents (status: ProofEngineTypes.status) =
-      let ((_, metasenv, _, _), goal) = status in
-      let sequents_no = List.length metasenv in
+    method load_sequents { proof = (_,metasenv,_,_) as proof; stack = stack } =
       _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 +603,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 = `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 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
 
@@ -533,7 +708,7 @@ let blank_uri = BuildTimeConf.blank_uri
 let current_proof_uri = BuildTimeConf.current_proof_uri
 
 type term_source =
-  [ `Ast of DisambiguateTypes.term
+  [ `Ast of CicNotationPt.term
   | `Cic of Cic.term * Cic.metasenv
   | `String of string
   ]
@@ -541,7 +716,6 @@ type term_source =
 class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   ()
 =
-  let term_RE = Pcre.regexp "^term:(.*)" in
   let whelp_RE = Pcre.regexp "^\\s*whelp" in
   let uri_RE =
     Pcre.regexp
@@ -549,8 +723,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   in
   let dir_RE = Pcre.regexp "^cic:((/([^/]+/)*[^/]+(/)?)|/|)$" in
   let whelp_query_RE = Pcre.regexp "^\\s*whelp\\s+([^\\s]+)\\s+(.*)$" in
-  let trailing_slash_RE = Pcre.regexp "/$" in
-  let has_xpointer_RE = Pcre.regexp "#xpointer\\(\\d+/\\d+(/\\d+)?\\)$" in
   let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in
   let is_uri txt = Pcre.pmatch ~rex:uri_RE txt in
   let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in
@@ -591,8 +763,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     try
       f ()
     with exn ->
-      if Helm_registry.get_bool "matita.catch_top_level_exn" then
-        fail (MatitaExcPp.to_string exn)
+      if not (Helm_registry.get_bool "matita.debug") then
+        fail (snd (MatitaExcPp.to_string exn))
       else raise exn
   in
   let handle_error' f = (fun () -> handle_error (fun () -> f ())) in
@@ -611,7 +783,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,11 +896,11 @@ 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 empty_mathml)#get_documentElement
 
     method private _loadCheck term =
       failwith "not implemented _loadCheck";
-      self#_showMath
+(*       self#_showMath *)
 
     method private egg () =
       win#mathOrListNotebook#goto_page 2;
@@ -736,12 +908,12 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
 
     method private home () =
       self#_showMath;
-      match self#script#status.proof_status with
+      match self#script#grafite_status.proof_status with
       | 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
-      | 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
@@ -769,7 +941,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       self#_loadList l
 
     method private setEntry entry =
-      win#browserUri#entry#set_text (string_of_entry entry);
+      win#browserUri#entry#set_text (MatitaTypes.string_of_entry entry);
       current_entry <- entry
 
     method private _loadObj obj =
@@ -805,17 +977,18 @@ 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
           | txt when is_uri txt -> `Uri (UriManager.uri_of_string (fix_uri txt))
           | txt when is_dir txt -> `Dir (MatitaMisc.normalize_dir txt)
           | txt ->
-              (try
-                entry_of_string txt
+             (try
+               MatitaTypes.entry_of_string txt
               with Invalid_argument _ ->
-                command_error (sprintf "unsupported uri: %s" txt))
+               raise
+                (GrafiteTypes.Command_error(sprintf "unsupported uri: %s" txt)))
         in
         self#_load entry;
         self#_historyAdd entry
@@ -834,7 +1007,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 () =
@@ -886,7 +1061,7 @@ let mathViewer () =
   end
 
 let refresh_all_browsers () =
- List.iter (fun b -> b#refresh ~force:false ()) !cicBrowsers
+  List.iter (fun b -> b#refresh ~force:false ()) !cicBrowsers
 
 let update_font_sizes () =
   List.iter (fun b -> b#updateFontSize) !cicBrowsers;
@@ -896,20 +1071,34 @@ let get_math_views () =
   ((cicMathView_instance ()) :> MatitaGuiTypes.clickableMathView)
   :: (List.map (fun b -> b#mathView) !cicBrowsers)
 
-let get_selections () =
-  if (MatitaScript.instance ())#onGoingProof () then
-    let rec aux =
-      function
-      | [] -> None
-      | mv :: tl ->
-          (match mv#string_of_selections with
-          | [] -> aux tl
-          | sels -> Some sels)
-    in
-    aux (get_math_views ())
-  else
-    None
-
-let reset_selections () =
-  List.iter (fun mv -> mv#remove_selections) (get_math_views ())
+let find_selection_owner () =
+  let rec aux =
+    function
+    | [] -> raise Not_found
+    | mv :: tl ->
+        (match mv#get_selections with
+        | [] -> aux tl
+        | sel :: _ -> mv)
+  in
+  aux (get_math_views ())
+
+let has_selection () =
+  try ignore (find_selection_owner ()); true
+  with Not_found -> false
+
+let math_view_clipboard = ref None (* associative list target -> string *)
+let has_clipboard () = !math_view_clipboard <> None
+let empty_clipboard () = math_view_clipboard := None
+
+let copy_selection () =
+  try
+    math_view_clipboard :=
+      Some ((find_selection_owner ())#strings_of_selection)
+  with Not_found -> failwith "no selection"
+
+let paste_clipboard paste_kind =
+  match !math_view_clipboard with
+  | None -> failwith "empty clipboard"
+  | Some cb ->
+      (try List.assoc paste_kind cb with Not_found -> assert false)