module Stack = Continuationals.Stack
-(** inherit from this class if you want to access current script *)
-class scriptAccessor =
-object (self)
- method private script = MatitaScript.current ()
-end
-
let cicBrowsers = ref []
let tab_label meta_markup =
class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
object (self)
- inherit scriptAccessor
-
method cicMathView = cicMathView (** clickableMathView accessor *)
val mutable pages = 0
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 = `Old []
+ val mutable _metasenv = [],[]
val mutable scrolledWin: GBin.scrolled_window option = None
(* scrolled window to which the sequentViewer is currently attached *)
val logo = (GMisc.image
page2goal <- [];
goal2page <- [];
goal2win <- [];
- _metasenv <- `Old [];
- self#script#setGoal None
+ _metasenv <- [],[]
method nload_sequents : 'status. #GrafiteTypes.status as 'status -> unit
= fun (status : #GrafiteTypes.status) ->
let _,_,metasenv,subst,_ = status#obj in
- _metasenv <- `New (metasenv,subst);
+ _metasenv <- metasenv,subst;
pages <- 0;
let win goal_switch =
let w =
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
+ (match cicMathView#misc#parent with
+ | None -> ()
+ | 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;
+ ignore (w#vadjustment#set_value
+ (w#vadjustment#upper -. w#vadjustment#page_size));
+ ignore (w#vadjustment#connect#changed (fun _ ->
+ w#vadjustment#set_value
+ (w#vadjustment#upper -. w#vadjustment#page_size)))
in
goal2win <- (goal_switch, reparent) :: goal2win;
w#coerce
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 status ~page ~goal_switch))
method private render_page:
= fun status ~page ~goal_switch ->
(match goal_switch with
| Stack.Open goal ->
- (match _metasenv with
- `Old menv -> assert false (* MATITA 1.0 *)
- | `New (menv,subst) ->
- cicMathView#nload_sequent status menv subst goal)
+ let menv,subst = _metasenv in
+ cicMathView#nload_sequent status menv subst goal
| Stack.Closed goal ->
let root = Lazy.force closed_goal_mathml in
cicMathView#load_root ~root);
let is_uri txt = Pcre.pmatch ~rex:uri_RE txt in
let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in
let gui = MatitaMisc.get_gui () in
- let (win: MatitaGuiTypes.browserWin) = gui#newBrowserWin () in
+ let win = new MatitaGeneratedGui.browserWin () in
+ let _ = win#browserUri#misc#grab_focus () in
let gviz = LablGraphviz.graphviz ~packing:win#graphScrolledWin#add () in
let searchText =
GSourceView2.source_view ~auto_indent:false ~editable:false ()
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
+ let status = (get_matita_script_current ())#status in
Pp.header
~name:"Hints"
~graph_type:"graph"
~name:"Coercions"
~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
~edge_attrs:["fontsize", "10"] fmt;
- let status = (MatitaScript.current ())#grafite_status in
+ let status = (get_matita_script_current ())#status in
NCicCoercion.generate_dot_file status fmt;
Pp.trailer fmt;
Pp.raw "@." fmt;
HExtlib.safe_remove filename
in
object (self)
- inherit scriptAccessor
-
val mutable gviz_uri = NReference.reference_of_string "cic:/dummy.dec";
val dep_contextual_menu = GMenu.menu ()
self#_showSearch
method private grammar () =
- self#_loadText (Print_grammar.ebnf_of_term self#script#grafite_status);
+ self#_loadText
+ (Print_grammar.ebnf_of_term (get_matita_script_current ())#status);
method private home () =
self#_showMath;
- match self#script#grafite_status#ng_mode with
- `ProofMode ->
- self#_loadNObj self#script#grafite_status
- self#script#grafite_status#obj
- | _ -> self#blank ()
+ let status = (get_matita_script_current ())#status in
+ match status#ng_mode with
+ `ProofMode -> self#_loadNObj status status#obj
+ | _ -> self#blank ()
method private _loadNReference (NReference.Ref (uri,_)) =
- let obj = NCicEnvironment.get_checked_obj uri in
- self#_loadNObj self#script#grafite_status obj
+ let status = (get_matita_script_current ())#status in
+ let obj = NCicEnvironment.get_checked_obj status uri in
+ self#_loadNObj status obj
method private _loadDir dir =
let content = Http_getter.ls ~local:false dir in
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
+ let status = (get_matita_script_current ())#status in
mathView#nload_sequent status m s d;
self#_showMath
self#_load entry;
self#_historyAdd entry
- (** {2 methods accessing underlying GtkMathView} *)
-
- method updateFontSize = mathView#set_font_size (MatitaMisc.get_current_font_size ())
-
(** {2 methods used by constructor only} *)
method win = win
=
(new sequentsViewer ~notebook ~cicMathView ():> MatitaGuiTypes.sequentsViewer)
-let cicBrowser () =
+let new_cicBrowser () =
let size = BuildTimeConf.browser_history_size in
let rec aux history =
let browser = new cicBrowser_impl ~history () in
GdkKeysyms._W (fun () -> win#toplevel#destroy ());
*)
cicBrowsers := browser :: !cicBrowsers;
- (browser :> MatitaGuiTypes.cicBrowser)
+ browser
in
let history = new MatitaMisc.browser_history size (`About `Blank) in
aux history
+(** @param reuse if set reused last opened cic browser otherwise
+* opens a new one. default is false *)
+let cicBrowser ?(reuse=false) t =
+ let browser =
+ if reuse then
+ (match !cicBrowsers with [] -> new_cicBrowser () | b :: _ -> b)
+ else
+ new_cicBrowser ()
+ in
+ match t with
+ None -> ()
+ | Some t -> browser#load t
+;;
+
let default_cicMathView () =
let res = cicMathView ~show:true () in
res#set_href_callback
(Some (fun uri ->
let uri = `NRef (NReference.reference_of_string uri) in
- (cicBrowser ())#load uri));
+ cicBrowser (Some uri)));
res
let cicMathView_instance =
MatitaMisc.singleton default_cicMathView
-let default_sequentsViewer () =
- let gui = MatitaMisc.get_gui () in
+let default_sequentsViewer notebook =
let cicMathView = cicMathView_instance () in
- sequentsViewer ~notebook:gui#main#sequentsNotebook ~cicMathView ()
-let sequentsViewer_instance = MatitaMisc.singleton default_sequentsViewer
-
-let mathViewer () =
- object(self)
- method private get_browser reuse =
- if reuse then
- (match !cicBrowsers with
- | [] -> cicBrowser ()
- | b :: _ -> (b :> MatitaGuiTypes.cicBrowser))
- else
- (cicBrowser ())
-
- method show_entry ?(reuse=false) t = (self#get_browser reuse)#load t
-
- method screenshot status sequents metasenv subst (filename as ofn) =
- () (*MATITA 1.0
- let w = GWindow.window ~title:"screenshot" () in
- let width = 500 in
- let height = 2000 in
- let m = GMathView.math_view
- ~font_size:(MatitaMisc.get_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
+ sequentsViewer ~notebook ~cicMathView ()
+
+let sequentsViewer_instance =
+ let already_used = ref false in
+ fun notebook ->
+ if !already_used then assert false
+ else
+ (already_used := true;
+ default_sequentsViewer notebook)
let refresh_all_browsers () =
List.iter (fun b -> b#refresh ~force:false ()) !cicBrowsers
-let update_font_sizes () =
- List.iter (fun b -> b#updateFontSize) !cicBrowsers;
- (cicMathView_instance ())#update_font_size
-
let get_math_views () =
(cicMathView_instance ()) :: (List.map (fun b -> b#mathView) !cicBrowsers)