X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaMathView.ml;h=10b7470a5b463f93661fd40f8a9331be1780e424;hb=6188c48d0ccbe5d8b7dbae9b8ff6de5bf984efa4;hp=5de25e45b13b784bca64eb50c5fafbe7d7341f99;hpb=f80a8edd258a2ca7fa27d8fbccafc11625460455;p=helm.git
diff --git a/matita/matitaMathView.ml b/matita/matitaMathView.ml
index 5de25e45b..10b7470a5 100644
--- a/matita/matitaMathView.ml
+++ b/matita/matitaMathView.ml
@@ -246,7 +246,6 @@ object (self)
| _ -> leave_href ())
| None -> leave_href ()
-
method private tactic_text_pattern_of_node node =
let id = id_of_node node in
let cic_info, unsh_sequent = self#get_cic_info id in
@@ -259,6 +258,16 @@ object (self)
| Some hyp_name -> None, [ hyp_name, text ], None)
| SelHyp (hyp_name, _ctxt) -> None, [ hyp_name, "%" ], None
+ method private tactic_text_of_node 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:`Term id in
+ let text = self#string_of_cic_sequent sequent in
+ text
+ | SelHyp (hyp_name, _ctxt) -> hyp_name
+
(** @return a pattern structure which contains pretty printed terms *)
method private tactic_text_pattern_of_selection =
match self#get_selections with
@@ -420,10 +429,13 @@ object (self)
method private string_of_node ~(paste_kind:paste_kind) node =
if node#hasAttributeNS ~namespaceURI:helm_ns ~localName:xref_ds
then
- let tactic_text_pattern = self#tactic_text_pattern_of_node node in
- GrafiteAstPp.pp_tactic_pattern
- ~term_pp:(fun s -> s) ~lazy_term_pp:(fun _ -> assert false)
- tactic_text_pattern
+ match paste_kind with
+ | `Pattern ->
+ let tactic_text_pattern = self#tactic_text_pattern_of_node node in
+ GrafiteAstPp.pp_tactic_pattern
+ ~term_pp:(fun s -> s) ~lazy_term_pp:(fun _ -> assert false)
+ tactic_text_pattern
+ | `Term -> self#tactic_text_of_node node
else string_of_dom_node node
method private string_of_cic_sequent cic_sequent =
@@ -571,8 +583,8 @@ end
let tab_label meta_markup =
let rec aux =
function
- | `Current m -> sprintf "%s" (aux m)
| `Closed m -> sprintf "%s" (aux m)
+ | `Current m -> sprintf "%s" (aux m)
| `Shift (pos, m) -> sprintf "|%d: %s" pos (aux m)
| `Meta n -> sprintf "?%d" n
in
@@ -694,7 +706,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
~env:(fun depth tag (pos, sw) ->
let markup =
match depth, pos with
- | 0, _ -> `Current (render_switch sw)
+ | 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
@@ -824,7 +837,18 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
in
let handle_error' f = (fun () -> handle_error (fun () -> f ())) in
let load_easter_egg = lazy (
- win#easterEggImage#set_file (MatitaMisc.image_path "meegg.png"))
+ win#browserImage#set_file (MatitaMisc.image_path "meegg.png"))
+ in
+ let load_coerchgraph () =
+ let str = CoercGraph.generate_dot_file () in
+ let filename, oc = Filename.open_temp_file "xx" ".dot" in
+ output_string oc str;
+ close_out oc;
+ let ps = Filename.temp_file "yy" ".png" in
+ ignore (Unix.system ("/usr/bin/dot -Tpng -o" ^ ps ^ " " ^ filename));
+ Sys.remove filename;
+ at_exit (fun _ -> Sys.remove ps);
+ win#browserImage#set_file ps
in
object (self)
inherit scriptAccessor
@@ -940,12 +964,14 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
* @param uri string *)
method private _load ?(force=false) entry =
handle_error (fun () ->
- if entry <> current_entry || entry = `About `Current_proof || force then
+ if entry <> current_entry || entry = `About `Current_proof || entry =
+ `About `Coercions || force then
begin
(match entry with
| `About `Current_proof -> self#home ()
| `About `Blank -> self#blank ()
| `About `Us -> self#egg ()
+ | `About `Coercions -> self#coerchgraph ()
| `Check term -> self#_loadCheck term
| `Cic (term, metasenv) -> self#_loadTermCic term metasenv
| `Dir dir -> self#_loadDir dir
@@ -969,6 +995,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
win#mathOrListNotebook#goto_page 2;
Lazy.force load_easter_egg
+ method private coerchgraph () =
+ win#mathOrListNotebook#goto_page 2;
+ load_coerchgraph ()
+
method private home () =
self#_showMath;
match self#script#grafite_status.proof_status with