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));
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 *)
in
let add_switch _ _ (_, sw) = add_tab (render_switch sw) sw in
Stack.iter (** populate notebook with tabs *)
method private render_page:
'status. #ApplyTransformation.status as 'status -> page:int ->
goal_switch:Stack.switch -> unit
method private render_page:
'status. #ApplyTransformation.status as 'status -> page:int ->
goal_switch:Stack.switch -> unit
(match goal_switch with
| Stack.Open goal ->
let menv,subst = _metasenv in
cicMathView#nload_sequent status menv subst goal
(match goal_switch with
| Stack.Open goal ->
let menv,subst = _metasenv in
cicMathView#nload_sequent status menv subst goal
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 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 win = new MatitaGeneratedGui.browserWin () in
let _ = win#browserUri#misc#grab_focus () in
let gviz = LablGraphviz.graphviz ~packing:win#graphScrolledWin#add () in
let searchText =
let win = new MatitaGeneratedGui.browserWin () in
let _ = win#browserUri#misc#grab_focus () in
let gviz = LablGraphviz.graphviz ~packing:win#graphScrolledWin#add () in
let searchText =
- ~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
- ~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;
method private redraw_gviz ?center_on () =
if Sys.command "which dot" = 0 then
let tmpfile, oc = Filename.open_temp_file "matita" ".dot" in
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;*)