open Printf
-open GrafiteTypes
open MatitaGtkMisc
-open MatitaGuiTypes
open CicMathView
module Stack = Continuationals.Stack
GtkSignal.disconnect notebook#as_widget id;
switch_page_callback <- None
| None -> ());
- for i = 0 to pages do notebook#remove_page 0 done;
+ for _i = 0 to pages do notebook#remove_page 0 done;
notebook#set_show_tabs true;
pages <- 0;
page2goal <- [];
goal2win <- [];
_metasenv <- [],[]
- method nload_sequents : 'status. #GrafiteTypes.status as 'status -> unit
+ method nload_sequents : 'status. (#GrafiteTypes.status as 'status) -> unit
= fun (status : #GrafiteTypes.status) ->
let _,_,metasenv,subst,_ = status#obj in
_metasenv <- metasenv,subst;
let win goal_switch =
let w =
GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`ALWAYS
- ~shadow_type:`IN ~show:true ()
- in
+ ~shadow_type:`IN ~show:true () 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 p ->
+ let parent = GContainer.cast_container p in
+ parent#remove cicMathView#coerce);
+ w#add cicMathView#coerce
in
goal2win <- (goal_switch, reparent) :: goal2win;
w#coerce
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)
- <> List.sort Pervasives.compare proof_goals
+ HExtlib.list_uniq (List.sort compare stack_goals)
+ <> List.sort 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));
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) ->
+ Stack.iter (* populate notebook with tabs *)
+ ~env:(fun depth _tag (pos, sw) ->
let markup =
match depth, pos with
| 0, 0 -> `Current (render_switch sw)
self#render_page status ~page ~goal_switch))
method private render_page:
- 'status. #ApplyTransformation.status as 'status -> page:int ->
+ 'status. (#ApplyTransformation.status as 'status) -> page:int ->
goal_switch:Stack.switch -> unit
- = fun status ~page ~goal_switch ->
+ = fun status ~page:_ ~goal_switch ->
(match goal_switch with
| Stack.Open goal ->
let menv,subst = _metasenv in
cicMathView#nload_sequent status menv subst goal
- | Stack.Closed goal ->
+ | Stack.Closed _goal ->
let root = Lazy.force closed_goal_mathml in
cicMathView#load_root ~root);
(try
cicMathView#set_selection None;
- List.assoc goal_switch goal2win ()
+ List.assoc goal_switch goal2win ();
+ (match cicMathView#misc#parent with
+ None -> assert false
+ | Some p ->
+ (* The text widget dinamycally inserts the text in a separate
+ thread. We need to wait for it to terminate before we can
+ move the scrollbar to the end *)
+ while Glib.Main.pending()do ignore(Glib.Main.iteration false); done;
+ let w =
+ new GBin.scrolled_window
+ (Gobject.try_cast p#as_widget "GtkScrolledWindow") in
+ (* The double change upper/lower is to trigger the emission of
+ changed :-( *)
+ w#hadjustment#set_value w#hadjustment#upper;
+ w#hadjustment#set_value w#hadjustment#lower;
+ w#vadjustment#set_value w#vadjustment#lower;
+ w#vadjustment#set_value
+ (w#vadjustment#upper -. w#vadjustment#page_size));
with Not_found -> assert false)
- method goto_sequent: 'status. #ApplyTransformation.status as 'status -> int -> unit
+ method goto_sequent: 'status. (#ApplyTransformation.status as 'status) -> int -> unit
= fun status goal ->
let goal_switch, page =
try
in
notebook#goto_page page;
self#render_page status ~page ~goal_switch
-
end
let blank_uri = BuildTimeConf.blank_uri
let dir_RE = Pcre.regexp "^cic:((/([^/]+/)*[^/]+(/)?)|/|)$" in
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 _gui = MatitaMisc.get_gui () 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 ()
+ GSourceView3.source_view ~auto_indent:false ~editable:false ()
in
let _ =
win#scrolledwinContent#add (searchText :> GObj.widget);
close_out oc;
if tred then
gviz#load_graph_from_file
- ~gviz_cmd:"dot -Txdot | tred |gvpack -gv | dot" filename
+ (* gvpack can no longer read the output of -Txdot :-( *)
+ (*~gviz_cmd:"dot -Txdot | tred |gvpack -gv | dot" filename*)
+ ~gviz_cmd:"dot -Txdot | tred | dot" filename
else
gviz#load_graph_from_file
- ~gviz_cmd:"dot -Txdot | gvpack -gv | dot" filename;
+ (* gvpack can no longer read the output of -Txdot :-( *)
+ (*~gviz_cmd:"dot -Txdot | gvpack -gv | dot" filename;*)
+ ~gviz_cmd:"dot -Txdot | dot" filename;
HExtlib.safe_remove filename
in
object (self)
- val mutable gviz_uri = NReference.reference_of_string "cic:/dummy.dec";
+ val mutable gviz_uri =
+ let uri = NUri.uri_of_string "cic:/dummy/dec.con" in
+ NReference.reference_of_spec uri NReference.Decl;
val dep_contextual_menu = GMenu.menu ()
self#_showMath;
mathView#load_root (Lazy.force empty_mathml)
- method private _loadCheck term =
+ method private _loadCheck _term =
failwith "not implemented _loadCheck";
(* self#_showMath *)
method private redraw_gviz ?center_on () =
if Sys.command "which dot" = 0 then
let tmpfile, oc = Filename.open_temp_file "matita" ".dot" in
- let fmt = Format.formatter_of_out_channel oc in
- (* MATITA 1.0 MetadataDeps.DepGraph.render fmt gviz_graph;*)
+ (* MATITA 1.0 let fmt = Format.formatter_of_out_channel oc in
+ MetadataDeps.DepGraph.render fmt gviz_graph;*)
close_out oc;
gviz#load_graph_from_file ~gviz_cmd:"tred | dot" tmpfile;
(match center_on with
"the graph of dependencies amoung objects. Please install it.")
~parent:win#toplevel ()
- method private dependencies direction uri () =
+ method private dependencies _direction _uri () =
assert false (* MATITA 1.0
let dbd = LibraryDb.instance () in
let graph =
(Virtuals.get_all_eqclass ()));
Printf.bprintf b "\n\nVirtual keys (trigger with ALT-L):\n\n";
List.iter
- (fun tag, items ->
+ (fun (tag, items) ->
Printf.bprintf b " %s:\n" tag;
List.iter
- (fun names, symbol ->
+ (fun (names, symbol) ->
Printf.bprintf b " \t%s\t%s\n"
(Glib.Utf8.from_unichar symbol)
(String.concat ", " names))
| _ -> self#blank ()
method private _loadNReference (NReference.Ref (uri,_)) =
- let obj = NCicEnvironment.get_checked_obj uri in
- self#_loadNObj (get_matita_script_current ())#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
let l =
List.fast_sort
- Pervasives.compare
+ compare
(List.map
(function
| Http_getter_types.Ls_section s -> "dir", s
| mv :: tl ->
(match mv#get_selections with
| [] -> aux tl
- | sel :: _ -> mv)
+ | _sel :: _ -> mv)
in
aux (get_math_views ())
projects / helm.git / blobdiff