X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaMathView.ml;h=271a7b19ab45c664f61aac4c805b435d81415044;hb=5d9f7ae4bad2b5926f615141c12942b9a8eb23fb;hp=df8b5359d98b72e54a1361960f008fe03dfc656d;hpb=eb42b31bafac10a5c5fb2a8baa9f448e3b2bfaaf;p=helm.git diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index df8b5359d..271a7b19a 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -27,9 +27,7 @@ open Printf -open GrafiteTypes open MatitaGtkMisc -open MatitaGuiTypes open CicMathView module Stack = Continuationals.Stack @@ -91,7 +89,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = 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 <- []; @@ -107,20 +105,15 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = 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 @@ -129,8 +122,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = 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)); @@ -159,7 +152,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = 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) @@ -181,17 +174,34 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = 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 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 @@ -205,7 +215,6 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = in notebook#goto_page page; self#render_page status ~page ~goal_switch - end let blank_uri = BuildTimeConf.blank_uri @@ -227,12 +236,12 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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); @@ -311,14 +320,20 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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 () @@ -458,7 +473,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) self#_showMath; mathView#load_root (Lazy.force empty_mathml) - method private _loadCheck term = + method private _loadCheck _term = failwith "not implemented _loadCheck"; (* self#_showMath *) @@ -469,8 +484,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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 @@ -483,7 +498,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) "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 = @@ -550,14 +565,15 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) | _ -> 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 @@ -633,7 +649,7 @@ let sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) (): = (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 @@ -651,17 +667,31 @@ let cicBrowser () = 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 = @@ -670,6 +700,7 @@ let cicMathView_instance = let default_sequentsViewer notebook = let cicMathView = cicMathView_instance () in sequentsViewer ~notebook ~cicMathView () + let sequentsViewer_instance = let already_used = ref false in fun notebook -> @@ -678,20 +709,6 @@ let sequentsViewer_instance = (already_used := true; default_sequentsViewer notebook) -(** @param reuse if set reused last opened cic browser otherwise -* opens a new one. default is false *) -let show_entry ?(reuse=false) t = - let browser = - if reuse then - (match !cicBrowsers with - [] -> cicBrowser () - | b :: _ -> (b :> MatitaGuiTypes.cicBrowser)) - else - cicBrowser () - in - browser#load t -;; - let refresh_all_browsers () = List.iter (fun b -> b#refresh ~force:false ()) !cicBrowsers @@ -705,7 +722,7 @@ let find_selection_owner () = | mv :: tl -> (match mv#get_selections with | [] -> aux tl - | sel :: _ -> mv) + | _sel :: _ -> mv) in aux (get_math_views ())