From: Claudio Sacerdoti Coen Date: Wed, 13 Nov 2002 19:04:39 +0000 (+0000) Subject: Interface improvements: the window to disambiguate uris is now reasonable. X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=85eee63b8b022bb73aaf4784b3d66262ed981e09;p=helm.git Interface improvements: the window to disambiguate uris is now reasonable. TODO: the stylesheets should be applied lazily for the pages of the notebook of the check window. --- diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index a1254be54..40e60b47e 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -90,6 +90,7 @@ let current_scratch_infos = ref None;; let id_to_uris = ref empty_id_to_uris;; let check_term = ref (fun _ _ _ -> assert false);; +let mml_of_cic_term_ref = ref (fun _ _ -> assert false);; exception RenderingWindowsNotInitialized;; @@ -115,6 +116,18 @@ let set_settings_window,settings_window = ) ;; +exception OutputHtmlNotInitialized;; + +let set_outputhtml,outputhtml = + let outputhtml_ref = ref None in + (function rw -> outputhtml_ref := Some rw), + (function () -> + match !outputhtml_ref with + None -> raise OutputHtmlNotInitialized + | Some outputhtml -> outputhtml + ) +;; + (* COMMAND LINE OPTIONS *) let usedb = ref true @@ -178,50 +191,145 @@ let string_of_cic_textual_parser_uri uri = String.sub uri' 4 (String.length uri' - 4) ;; +let output_html outputhtml msg = + htmlheader_and_content := !htmlheader_and_content ^ msg ; + outputhtml#source (!htmlheader_and_content ^ htmlfooter) ; + outputhtml#set_topline (-1) +;; + (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *) +(* Check window *) + +let check_window outputhtml uris_and_terms = + let window = + GWindow.window + ~width:800 ~modal:true ~title:"Check" ~border_width:2 () in + let notebook = + GPack.notebook ~scrollable:true ~packing:window#add () in + ignore ( + List.map + (function (uri,expr) -> + let scrolled_window = + GBin.scrolled_window ~border_width:10 + ~packing: + (notebook#append_page + ~tab_label:((GMisc.label ~text:uri ())#coerce) + ) + () in + let mmlwidget = + GMathView.math_view + ~packing:(scrolled_window#add) ~width:400 ~height:280 () in + try + let mml = !mml_of_cic_term_ref 111 expr in +prerr_endline ("### " ^ CicPp.ppterm expr) ; + mmlwidget#load_tree ~dom:mml + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") + ) uris_and_terms) ; + window#show () +;; + exception NoChoice;; -let interactive_user_uri_choice ?(cancel="Cancel") ~title ~msg uris = - let choice = ref None in - let window = GWindow.dialog ~modal:true ~title () in +let + interactive_user_uri_choice ~selection_mode ?(ok="Ok") ~title ~msg uris += + let choices = ref [] in + let chosen = ref false in + let window = + GWindow.dialog ~modal:true ~title ~width:600 () in let lMessage = - GMisc.label ~text:msg ~packing:window#vbox#add () in - let vbox = GPack.vbox ~border_width:10 - ~packing:(window#action_area#pack ~expand:true ~padding:4) () in - let hbox1 = GPack.hbox ~border_width:10 ~packing:vbox#add () in - let combo = - GEdit.combo ~popdown_strings:uris ~packing:hbox1#add () in - let checkb = - GButton.button ~label:"Check" - ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in - let hbox = GPack.hbox ~border_width:10 ~packing:vbox#add () in + GMisc.label ~text:msg + ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in + let scrolled_window = + GBin.scrolled_window ~border_width:10 + ~packing:(window#vbox#pack ~expand:true ~fill:true ~padding:5) () in + let clist = + let expected_height = 8 * List.length uris in + let height = if expected_height > 400 then 400 else expected_height in + GList.clist ~columns:1 ~packing:scrolled_window#add + ~height ~selection_mode () in + let _ = List.map (function x -> clist#append [x]) uris in + let hbox2 = + GPack.hbox ~border_width:0 + ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in + let explain_label = + GMisc.label ~text:"None of the above. Try this one:" + ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in + let manual_input = + GEdit.entry ~editable:true + ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in + let hbox = + GPack.hbox ~border_width:0 ~packing:window#action_area#add () in let okb = - GButton.button ~label:"Ok" + GButton.button ~label:ok ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = okb#misc#set_sensitive false in + let checkb = + GButton.button ~label:"Check" + ~packing:(hbox#pack ~padding:5) () in + let _ = checkb#misc#set_sensitive false in let cancelb = - GButton.button ~label:cancel + GButton.button ~label:"Abort" ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in (* actions *) - let ok_callback () = - choice := Some combo#entry#text ; - window#destroy () - in let check_callback () = - !check_term [] [] - (term_of_cic_textual_parser_uri - (cic_textual_parser_uri_of_string combo#entry#text)) + assert (List.length !choices > 0) ; + check_window (outputhtml ()) + (List.map + (function uri -> + let term = + term_of_cic_textual_parser_uri + (cic_textual_parser_uri_of_string uri) + in + uri, + (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term)) + ) !choices) in ignore (window#connect#destroy GMain.Main.quit) ; ignore (cancelb#connect#clicked window#destroy) ; - ignore (okb#connect#clicked ok_callback) ; + ignore + (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ; ignore (checkb#connect#clicked check_callback) ; + ignore + (clist#connect#select_row + (fun ~row ~column ~event -> + checkb#misc#set_sensitive true ; + okb#misc#set_sensitive true ; + choices := (List.nth uris row)::!choices)) ; + ignore + (clist#connect#unselect_row + (fun ~row ~column ~event -> + choices := + List.filter (function uri -> uri != (List.nth uris row)) !choices)) ; + ignore + (manual_input#connect#changed + (fun _ -> + if manual_input#text = "" then + begin + choices := [] ; + checkb#misc#set_sensitive false ; + okb#misc#set_sensitive false ; + clist#misc#set_sensitive true + end + else + begin + choices := [manual_input#text] ; + clist#unselect_all () ; + checkb#misc#set_sensitive true ; + okb#misc#set_sensitive true ; + clist#misc#set_sensitive false + end)); window#set_position `CENTER ; window#show () ; GMain.Main.main () ; - match !choice with - None -> raise NoChoice - | Some uri -> uri + if !chosen or List.length !choices > 0 then + !choices + else + raise NoChoice ;; (* MISC FUNCTIONS *) @@ -241,12 +349,6 @@ let register_alias (id,uri) = function id' -> if id' = id then Some uri else resolve_id id' ;; -let output_html outputhtml msg = - htmlheader_and_content := !htmlheader_and_content ^ msg ; - outputhtml#source (!htmlheader_and_content ^ htmlfooter) ; - outputhtml#set_topline (-1) -;; - let locate_one_id id = let result = MQueryGenerator.locate id in let uris = @@ -268,17 +370,14 @@ let locate_one_id id = ) | [uri] -> [uri] | _ -> - try - [interactive_user_uri_choice - ~cancel:"Try every possibility." - ~title:"Ambiguous input." - ~msg: - ("Ambiguous input \"" ^ id ^ - "\". Please, choose one interpretation:") - uris - ] - with - NoChoice -> uris + interactive_user_uri_choice + ~selection_mode:`EXTENDED + ~ok:"Try all the sections." + ~title:"Ambiguous input." + ~msg: + ("Ambiguous input \"" ^ id ^ + "\". Please, choose one or more interpretations:") + uris in List.map cic_textual_parser_uri_of_string uris' ;; @@ -1423,7 +1522,11 @@ let user_uri_choice ~title ~msg uris = [] -> raise NoObjectsLocated | [uri] -> uri | uris -> - interactive_user_uri_choice ~title ~msg uris + match + interactive_user_uri_choice ~selection_mode:`SINGLE ~title ~msg uris + with + [uri] -> uri + | _ -> assert false in String.sub uri 4 (String.length uri - 4) ;; @@ -2005,6 +2108,7 @@ object let settings_window = new settings_window output scrolled_window0 export_to_postscript_menu_item (choose_selection output) in set_settings_window settings_window ; + set_outputhtml outputhtml ; ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ; ignore(stateb#connect#clicked state) ; ignore(openb#connect#clicked open_) ; @@ -2023,6 +2127,7 @@ let initialize_everything () = let notebook = new notebook in let rendering_window' = new rendering_window output notebook in set_rendering_window rendering_window' ; + mml_of_cic_term_ref := mml_of_cic_term ; rendering_window'#show () ; GMain.Main.main () ;;