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 <- [];
scrolledWin <- Some w;
(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
+ | Some p ->
+ let parent = GContainer.cast_container p in
parent#remove cicMathView#coerce);
w#add cicMathView#coerce
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)
- <> 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));
in
let add_switch _ _ (_, sw) = add_tab (render_switch sw) sw in
Stack.iter (** populate notebook with tabs *)
- ~env:(fun depth tag (pos, sw) ->
+ ~env:(fun depth _tag (pos, sw) ->
let markup =
match depth, pos with
| 0, 0 -> `Current (render_switch sw)
method private render_page:
'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
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)
self#_showMath;
mathView#load_root (Lazy.force empty_mathml)
- method private _loadCheck term =
+ method private _loadCheck _term =
failwith "not implemented _loadCheck";
(* self#_showMath *)
"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 =
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 ())