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;;
)
;;
+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
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
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ ) 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 *)
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 =
)
| [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'
;;
[] -> 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)
;;
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_) ;
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 ()
;;
projects / helm.git / commitdiff