end;
self#load_root ~root:mathml#get_documentElement
- method nload_sequent metasenv subst metano =
+ method nload_sequent:
+ 'status. #NCicCoercion.status as 'status -> NCic.metasenv ->
+ NCic.substitution -> int -> unit
+ = fun status metasenv subst metano ->
let sequent = List.assoc metano metasenv in
let mathml =
- ApplyTransformation.nmml_of_cic_sequent metasenv subst (metano,sequent)
+ ApplyTransformation.nmml_of_cic_sequent status metasenv subst
+ (metano,sequent)
in
if BuildTimeConf.debug then begin
let name =
end;
self#load_root ~root:mathml#get_documentElement;
current_mathml <- Some mathml);
+
+ method load_nobject :
+ 'status. #NCicCoercion.status as 'status -> NCic.obj -> unit
+ = fun status obj ->
+ let mathml = ApplyTransformation.nmml_of_cic_object status obj in
+(*
+ self#set_cic_info
+ (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;
+ XmlDiff.update_dom ~from:current_mathml mathml;
+ self#thaw
+ | _ ->
+*)
+ if BuildTimeConf.debug then begin
+ let name =
+ "/tmp/cic_browser_" ^ string_of_int (Unix.getuid ()) ^ ".xml" in
+ HLog.debug ("cic_browser: dumping MathML to ./" ^ name);
+ ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ())
+ end;
+ self#load_root ~root:mathml#get_documentElement;
+ (*current_mathml <- Some mathml*)(*)*);
end
let tab_label meta_markup =
_metasenv <- `Old [];
self#script#setGoal None
- method load_sequents
- { proof = (_,metasenv,_subst,_,_, _) as proof; stack = stack }
- =
+ method load_sequents : 'status. #NCicCoercion.status as 'status -> 'a
+ = fun status { proof= (_,metasenv,_subst,_,_, _) as proof; stack = stack }
+ ->
_metasenv <- `Old metasenv;
pages <- 0;
let win 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))
+ self#render_page status ~page ~goal_switch))
- method nload_sequents
- { NTacStatus.istatus = { NTacStatus.pstatus = (_,_,metasenv,subst,_) }; gstatus = stack }
- =
+ method nload_sequents : 'status. #NTacStatus.tac_status as 'status -> unit
+ = fun status ->
+ let _,_,metasenv,subst,_ = status#obj in
_metasenv <- `New (metasenv,subst);
pages <- 0;
let win goal_switch =
w#coerce
in
assert (
- let stack_goals = Stack.open_goals stack in
+ let stack_goals = Stack.open_goals status#stack in
let proof_goals = List.map fst metasenv in
if
HExtlib.list_uniq (List.sort Pervasives.compare stack_goals)
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 ->
+ | 1, pos when Stack.head_tag status#stack = `BranchTag ->
`Shift (pos, render_switch sw)
| _ -> render_switch sw
in
add_tab markup sw)
~cont:add_switch ~todo:add_switch
- stack;
+ status#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))
+ self#render_page status ~page ~goal_switch))
- method private render_page ~page ~goal_switch =
+ method private render_page:
+ 'status. #NCicCoercion.status as 'status -> page:int ->
+ goal_switch:Stack.switch -> unit
+ = fun status ~page ~goal_switch ->
(match goal_switch with
| Stack.Open goal ->
(match _metasenv with
`Old menv -> cicMathView#load_sequent menv goal
- | `New (menv,subst) -> cicMathView#nload_sequent menv subst goal)
+ | `New (menv,subst) ->
+ cicMathView#nload_sequent status menv subst goal)
| Stack.Closed goal ->
let doc = Lazy.force closed_goal_mathml in
cicMathView#load_root ~root:doc#get_documentElement);
List.assoc goal_switch goal2win ()
with Not_found -> assert false)
- method goto_sequent goal =
+ method goto_sequent: 'status. #NCicCoercion.status as 'status -> int -> unit
+ = fun status goal ->
let goal_switch, page =
try
List.find
with Not_found -> assert false
in
notebook#goto_page page;
- self#render_page page goal_switch
+ self#render_page status ~page ~goal_switch
end
type term_source =
[ `Ast of CicNotationPt.term
| `Cic of Cic.term * Cic.metasenv
+ | `NCic of NCic.term * NCic.context * NCic.metasenv * NCic.substitution
| `String of string
]
let dir_RE = Pcre.regexp "^cic:((/([^/]+/)*[^/]+(/)?)|/|)$" in
let metadata_RE = Pcre.regexp "^metadata:/(deps)/(forward|backward)/(.*)$" in
let whelp_query_RE = Pcre.regexp
- "^\\s*whelp\\s+([^\\s]+)\\s+(\"|\\()(.*)(\\)|\")$"
+ "^\\s*whelp\\s+([^\\s]+)\\s+(.*)$"
in
let is_metadata txt = Pcre.pmatch ~rex:metadata_RE txt in
let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in
combo#set_active (aux 0 queries);
in
let searchText =
- GSourceView.source_view ~auto_indent:false ~editable:false ()
+ GSourceView2.source_view ~auto_indent:false ~editable:false ()
in
let _ =
win#scrolledwinContent#add (searchText :> GObj.widget);
let load_easter_egg = lazy (
win#browserImage#set_file (MatitaMisc.image_path "meegg.png"))
in
+ let load_hints () =
+ 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
+ Pp.header
+ ~name:"Hints"
+ ~graph_type:"graph"
+ ~graph_attrs:["overlap", "false"]
+ ~node_attrs:["fontsize", "9"; "width", ".4";
+ "height", ".4"; "shape", "box"]
+ ~edge_attrs:["fontsize", "10"; "len", "2"] fmt;
+ NCicUnifHint.generate_dot_file status fmt;
+ Pp.trailer fmt;
+ Pp.raw "@." fmt;
+ close_out oc;
+ gviz#load_graph_from_file ~gviz_cmd:"neato -Tpng" filename;
+ (*HExtlib.safe_remove filename*)
+ in
let load_coerchgraph tred () =
- let str = CoercGraph.generate_dot_file () in
+ let module Pp = GraphvizPp.Dot in
let filename, oc = Filename.open_temp_file "matita" ".dot" in
- output_string oc str;
+ let fmt = Format.formatter_of_out_channel oc in
+ Pp.header
+ ~name:"Coercions"
+ ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
+ ~edge_attrs:["fontsize", "10"] fmt;
+ let status = (MatitaScript.current ())#grafite_status in
+ NCicCoercion.generate_dot_file status fmt;
+ Pp.trailer fmt;
+ Pp.header
+ ~name:"OLDCoercions"
+ ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
+ ~edge_attrs:["fontsize", "10"] fmt;
+ CoercGraph.generate_dot_file fmt;
+ Pp.trailer fmt;
+ Pp.raw "@." fmt;
close_out oc;
if tred then
- gviz#load_graph_from_file ~gviz_cmd:"tred|dot" filename
+ gviz#load_graph_from_file
+ ~gviz_cmd:"dot -Txdot | tred |gvpack -gv | dot" filename
else
- gviz#load_graph_from_file filename;
+ gviz#load_graph_from_file
+ ~gviz_cmd:"dot -Txdot | gvpack -gv | dot" filename;
HExtlib.safe_remove filename
in
object (self)
handle_error (fun () -> self#loadInput (self#_getSelectedUri ()))));
mathView#set_href_callback (Some (fun uri ->
handle_error (fun () ->
- self#load (`Uri (UriManager.uri_of_string uri)))));
+ let uri =
+ try
+ `Uri (UriManager.uri_of_string uri)
+ with
+ UriManager.IllFormedUri _ ->
+ `NRef (NReference.reference_of_string uri)
+ in
+ self#load uri)));
gviz#connect_href (fun button_ev attrs ->
let time = GdkEvent.Button.time button_ev in
let uri = List.assoc "href" attrs in
| `About `Us -> self#egg ()
| `About `CoercionsFull -> self#coerchgraph false ()
| `About `Coercions -> self#coerchgraph true ()
+ | `About `Hints -> self#hints ()
| `About `TeX -> self#tex ()
| `About `Grammar -> self#grammar ()
| `Check term -> self#_loadCheck term
| `Cic (term, metasenv) -> self#_loadTermCic term metasenv
+ | `NCic (term, ctx, metasenv, subst) ->
+ self#_loadTermNCic term metasenv subst ctx
| `Dir dir -> self#_loadDir dir
| `HBugs `Tutors -> self#_loadHBugsTutors
| `Metadata (`Deps ((`Fwd | `Back) as dir, uri)) ->
self#dependencies dir uri ()
| `Uri uri -> self#_loadUriManagerUri uri
+ | `NRef nref -> self#_loadNReference nref
| `Univs uri -> self#_loadUnivs uri
| `Whelp (query, results) ->
- set_whelp_query query;
self#_loadList (List.map (fun r -> "obj",
UriManager.string_of_uri r) results));
self#setEntry entry
load_coerchgraph tred ();
self#_showGviz
+ method private hints () =
+ load_hints ();
+ self#_showGviz
+
method private tex () =
let b = Buffer.create 1000 in
Printf.bprintf b "UTF-8 equivalence classes (rotate with ALT-L):\n\n";
method private home () =
self#_showMath;
- match self#script#grafite_status.proof_status with
+ match self#script#grafite_status#proof_status with
| Proof (uri, metasenv, _subst, bo, ty, attrs) ->
- let name = UriManager.name_of_uri (HExtlib.unopt uri) in
- let obj = Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs) in
+ let name = UriManager.name_of_uri (HExtlib.unopt uri) in
+ let obj =
+ Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs)
+ in
self#_loadObj obj
| Incomplete_proof { proof = (uri, metasenv, _subst, bo, ty, attrs) } ->
- let name = UriManager.name_of_uri (HExtlib.unopt uri) in
- let obj = Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs) in
+ let name = UriManager.name_of_uri (HExtlib.unopt uri) in
+ let obj =
+ Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs)
+ in
self#_loadObj obj
- | _ -> self#blank ()
+ | _ ->
+ match self#script#grafite_status#ng_mode with
+ `ProofMode ->
+ self#_loadNObj self#script#grafite_status
+ self#script#grafite_status#obj
+ | _ -> self#blank ()
(** loads a cic uri from the environment
* @param uri UriManager.uri *)
let (obj, _) = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
self#_loadObj obj
+ method private _loadNReference (NReference.Ref (uri,_)) =
+ let obj = NCicEnvironment.get_checked_obj uri in
+ self#_loadNObj self#script#grafite_status obj
+
method private _loadUnivs uri =
let uri = UriManager.strip_xpointer uri in
let (_, u) = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
self#_showMath;
mathView#load_object obj
+ method private _loadNObj status obj =
+ (* showMath must be done _before_ loading the document, since if the
+ * widget is not mapped (hidden by the notebook) the document is not
+ * rendered *)
+ self#_showMath;
+ mathView#load_nobject status obj
+
method private _loadTermCic term metasenv =
let context = self#script#proofContext in
let dummyno = CicMkImplicit.new_meta metasenv [] in
mathView#load_sequent (sequent :: metasenv) dummyno;
self#_showMath
+ 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
+ mathView#nload_sequent status m s d;
+ self#_showMath
+
method private _loadList l =
model#list_store#clear ();
List.iter (fun (tag, s) -> model#easy_append ~tag s) l;
method show_uri_list ?(reuse=false) ~entry l =
(self#get_browser reuse)#load entry
+
+ method screenshot status sequents metasenv subst (filename as ofn) =
+ let w = GWindow.window ~title:"screenshot" () in
+ let width = 500 in
+ let height = 2000 in
+ let m = GMathView.math_view
+ ~font_size:!current_font_size ~width ~height
+ ~packing:w#add
+ ~show:true ()
+ in
+ w#show ();
+ let filenames =
+ HExtlib.list_mapi
+ (fun (mno,_ as sequent) i ->
+ let mathml =
+ ApplyTransformation.nmml_of_cic_sequent
+ status metasenv subst sequent
+ in
+ m#load_root ~root:mathml#get_documentElement;
+ let pixmap = m#get_buffer in
+ let pixbuf = GdkPixbuf.create ~width ~height () in
+ GdkPixbuf.get_from_drawable ~dest:pixbuf pixmap;
+ let filename =
+ filename ^ "-raw" ^ string_of_int i ^ ".png"
+ in
+ GdkPixbuf.save ~filename ~typ:"png" pixbuf;
+ filename,mno)
+ sequents
+ in
+ let items =
+ List.map (fun (x,mno) ->
+ ignore(Sys.command
+ (Printf.sprintf
+ ("convert "^^
+ " '(' -gravity west -bordercolor grey -border 1 label:%d ')' "^^
+ " '(' -trim -bordercolor white -border 5 "^^
+ " -bordercolor grey -border 1 %s ')' -append %s ")
+ mno
+ (Filename.quote x)
+ (Filename.quote (x ^ ".label.png"))));
+ x ^ ".label.png")
+ filenames
+ in
+ let rec div2 = function
+ | [] -> []
+ | [x] -> [[x]]
+ | x::y::tl -> [x;y] :: div2 tl
+ in
+ let items = div2 items in
+ ignore(Sys.command (Printf.sprintf
+ "convert %s -append %s"
+ (String.concat ""
+ (List.map (fun items ->
+ Printf.sprintf " '(' %s +append ')' "
+ (String.concat
+ (" '(' -gravity center -size 10x10 xc: ')' ") items)) items))
+ (Filename.quote (ofn ^ ".png"))));
+ List.iter (fun x,_ -> Sys.remove x) filenames;
+ List.iter Sys.remove (List.flatten items);
+ w#destroy ();
end
let refresh_all_browsers () =
projects / helm.git / blobdiff