-(* Copyright (C) 2000-2003, HELM Team.
+(* Copyright (C) 2000-2004, HELM Team.
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
(* *)
(******************************************************************************)
-open Printf;;
+let debug_level = ref 1
+let debug_print ?(level = 1) s = if !debug_level >= level then prerr_endline s
+
+open Printf
(* DEBUGGING *)
(* GLOBAL CONSTANTS *)
-let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log] (* default MathQL interpreter options *)
-(*
-let mqi_flags = [] (* default MathQL interpreter options *)
-*)
-let mqi_handle = MQIC.init mqi_flags prerr_string
+let mqi_debug_fun s = debug_print ~level:2 s
+let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log]
+let mqi_handle = MQIC.init mqi_flags mqi_debug_fun
let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
let restore_environment_on_boot = true ;;
let notify_hbugs_on_goal_change = false ;;
+let auto_disambiguation = ref true ;;
+
(* GLOBAL REFERENCES (USED BY CALLBACKS) *)
let check_term = ref (fun _ _ _ -> assert false);;
interactive_user_uri_choice ~(selection_mode:[`MULTIPLE|`SINGLE]) ?(ok="Ok")
?(enable_button_for_non_vars=false) ~title ~msg uris
=
- let choices = ref [] in
- let chosen = ref false in
- let use_only_constants = ref false in
- let window =
- GWindow.dialog ~modal:true ~title ~width:600 () in
- let lMessage =
- 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 = 18 * 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:(selection_mode :> Gtk.Tags.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
- ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
- let _ = okb#misc#set_sensitive false in
- let nonvarsb =
- GButton.button
- ~packing:
- (function w ->
- if enable_button_for_non_vars then
- hbox#pack ~expand:false ~fill:false ~padding:5 w)
- ~label:"Try constants only" () 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:"Abort"
- ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
- (* actions *)
- let check_callback () =
- assert (List.length !choices > 0) ;
- check_window (outputhtml ()) !choices
+ let only_constant_choices =
+ lazy
+ (List.filter
+ (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
+ uris)
in
- ignore (window#connect#destroy GMain.Main.quit) ;
- ignore (cancelb#connect#clicked window#destroy) ;
- ignore
- (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
- ignore
- (nonvarsb#connect#clicked
- (function () ->
- use_only_constants := true ;
- 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 () ;
+ if !auto_disambiguation then
+ Lazy.force only_constant_choices
+ else begin
+ let choices = ref [] in
+ let chosen = ref false in
+ let use_only_constants = ref false in
+ let window =
+ GWindow.dialog ~modal:true ~title ~width:600 () in
+ let lMessage =
+ 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 = 18 * 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:(selection_mode :> Gtk.Tags.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
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let _ = okb#misc#set_sensitive false in
+ let nonvarsb =
+ GButton.button
+ ~packing:
+ (function w ->
+ if enable_button_for_non_vars then
+ hbox#pack ~expand:false ~fill:false ~padding:5 w)
+ ~label:"Try constants only" () in
+ let autob =
+ GButton.button
+ ~packing:
+ (fun w ->
+ if enable_button_for_non_vars then
+ hbox#pack ~expand:false ~fill:false ~padding:5 w)
+ ~label:"Auto" () 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:"Abort"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ (* actions *)
+ let check_callback () =
+ assert (List.length !choices > 0) ;
+ check_window (outputhtml ()) !choices
+ in
+ ignore (window#connect#destroy GMain.Main.quit) ;
+ ignore (cancelb#connect#clicked window#destroy) ;
+ ignore
+ (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
+ ignore
+ (nonvarsb#connect#clicked
+ (function () ->
+ use_only_constants := true ;
+ chosen := true ;
+ window#destroy ()
+ )) ;
+ ignore (autob#connect#clicked (fun () ->
+ auto_disambiguation := true;
+ (rendering_window ())#set_auto_disambiguation true;
+ use_only_constants := true ;
+ 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 ;
- clist#misc#set_sensitive false
- end));
- window#set_position `CENTER ;
- window#show () ;
- GtkThread.main ();
- if !chosen then
- if !use_only_constants then
- List.filter
- (function uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
- uris
- else
- if List.length !choices > 0 then !choices else raise NoChoice
- else
- raise NoChoice
+ 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 () ;
+ GtkThread.main ();
+ if !chosen then
+ if !use_only_constants then
+ Lazy.force only_constant_choices
+ else
+ if List.length !choices > 0 then !choices else raise NoChoice
+ else
+ raise NoChoice
+ end
;;
let interactive_interpretation_choice interpretations =
)
;;
-let mk_fresh_name_callback context name ~typ =
+let mk_fresh_name_callback metasenv context name ~typ =
let fresh_name =
- match ProofEngineHelpers.mk_fresh_name context name ~typ with
+ match FreshNamesGenerator.mk_fresh_name metasenv context name ~typ with
Cic.Name fresh_name -> fresh_name
| Cic.Anonymous -> assert false
in
match ProofEngine.get_proof () with
None -> assert false
| Some (uri,metasenv,bo,ty) ->
-prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
- raise (InvokeTactics.RefreshProofException e)
+ debug_print ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[])));
+ raise (InvokeTactics.RefreshProofException e)
let set_proof_engine_goal g =
ProofEngine.goal := g
| Some (_,metasenv,_,_) -> metasenv
in
try
-let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
- prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
- raise (InvokeTactics.RefreshSequentException e)
-with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unknown."); raise (InvokeTactics.RefreshSequentException e)
+ let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
+ debug_print
+ ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent);
+ raise (InvokeTactics.RefreshSequentException e)
+with Not_found ->
+ debug_print ("Offending sequent " ^ string_of_int metano ^ " unknown.");
+ raise (InvokeTactics.RefreshSequentException e)
module InvokeTacticsCallbacks =
struct
(`Error (`T (Printexc.to_string e)))
;;
+let clear_aliases () =
+ let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
+ inputt#environment :=
+ DisambiguatingParser.EnvironmentP3.of_string
+ DisambiguatingParser.EnvironmentP3.empty
+;;
+
let edit_aliases () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let id_to_uris = inputt#id_to_uris in
- let chosen = ref false in
+ let disambiguation_env = inputt#environment in
+ let chosen_aliases = ref None in
let window =
GWindow.window
~width:400 ~modal:true ~title:"Edit Aliases..." ~border_width:2 () in
let okb =
GButton.button ~label:"Ok"
~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let clearb =
+ GButton.button ~label:"Clear"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
let cancelb =
GButton.button ~label:"Cancel"
~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
ignore (window#connect#destroy GMain.Main.quit) ;
ignore (cancelb#connect#clicked window#destroy) ;
- ignore
- (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
- let dom,resolve_id = !id_to_uris in
+ ignore (clearb#connect#clicked (fun () ->
+ input#buffer#set_text DisambiguatingParser.EnvironmentP3.empty)) ;
+ ignore (okb#connect#clicked (fun () ->
+ chosen_aliases := Some (input#buffer#get_text ());
+ window#destroy ()));
ignore
(input#buffer#insert ~iter:(input#buffer#get_iter_at_char 0)
- (String.concat "\n"
- (List.map
- (function v ->
- let uri =
- match resolve_id v with
- None -> assert false
- | Some (CicTextualParser0.Uri uri) -> uri
- | Some (CicTextualParser0.Term _)
- | Some CicTextualParser0.Implicit -> assert false
- in
- "alias " ^
- (match v with
- CicTextualParser0.Id id -> id
- | CicTextualParser0.Symbol (descr,_) ->
- (* CSC: To be implemented *)
- assert false
- )^ " " ^ (string_of_cic_textual_parser_uri uri)
- ) dom))) ;
+ (DisambiguatingParser.EnvironmentP3.to_string !disambiguation_env ^ "\n"));
window#show () ;
GtkThread.main ();
- if !chosen then
- let dom,resolve_id =
- let inputtext = input#buffer#get_text () in
- let regexpr =
- let alfa = "[a-zA-Z_-]" in
- let digit = "[0-9]" in
- let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in
- let blanks = "\( \|\t\|\n\)+" in
- let nonblanks = "[^ \t\n]+" in
- let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *)
- Str.regexp
- ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)")
- in
- let rec aux n =
- try
- let n' = Str.search_forward regexpr inputtext n in
- let id = CicTextualParser0.Id (Str.matched_group 2 inputtext) in
- let uri =
- MQueryMisc.cic_textual_parser_uri_of_string
- ("cic:" ^ (Str.matched_group 5 inputtext))
- in
- let dom,resolve_id = aux (n' + 1) in
- if List.mem id dom then
- dom,resolve_id
- else
- id::dom,
- (function id' ->
- if id = id' then
- Some (CicTextualParser0.Uri uri)
- else resolve_id id')
- with
- Not_found -> TermEditor.empty_id_to_uris
- in
- aux 0
- in
- id_to_uris := (dom,resolve_id)
+ match !chosen_aliases with
+ | None -> ()
+ | Some raw_aliases ->
+ let new_disambiguation_env =
+ (try
+ DisambiguatingParser.EnvironmentP3.of_string raw_aliases
+ with e ->
+ output_html (outputhtml ())
+ (`Error (`T
+ ("Error while parsing aliases: " ^ Printexc.to_string e)));
+ !disambiguation_env)
+ in
+ disambiguation_env := new_disambiguation_env
;;
let proveit () =
let module G = Gdome in
let notebook = (rendering_window ())#notebook in
let output = (rendering_window ())#output in
- let outputhtml = ((rendering_window ())#outputhtml (*: GHtml.xmhtml*)) in
+ let outputhtml = (rendering_window ())#outputhtml in
try
output#make_sequent_of_selected_term ;
refresh_proof output ;
Cic2acic.acic_object_of_cic_object obj
in
let mml =
- ApplyStylesheets.mml_of_cic_object
+ ChosenTransformer.mml_of_cic_object
~explode_all:false uri acic ids_to_inner_sorts ids_to_inner_types
in
window#set_title (UriManager.string_of_uri uri) ;
(* A WIDGET TO ENTER CIC TERMS *)
-module ChosenTermEditor = TexTermEditor;;
-module ChosenTextualParser0 = TexCicTextualParser0;;
-(*
-module ChosenTermEditor = TermEditor;;
-module ChosenTextualParser0 = CicTextualParser0;;
-*)
-
-module Callbacks =
+module DisambiguateCallbacks =
struct
- let get_metasenv () = !ChosenTextualParser0.metasenv
- let set_metasenv metasenv = ChosenTextualParser0.metasenv := metasenv
-
let output_html ?append_NL = output_html ?append_NL (outputhtml ())
let interactive_user_uri_choice =
fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id ->
end
;;
-module TexTermEditor' = ChosenTermEditor.Make(Callbacks);;
+module TermEditor' = ChosenTermEditor.Make (DisambiguateCallbacks);;
(* OTHER FUNCTIONS *)
GBin.scrolled_window ~border_width:5
~packing:(vbox#pack ~expand:true ~padding:0) () in
let newinputt =
- TexTermEditor'.term_editor
+ TermEditor'.term_editor
mqi_handle
~width:400 ~height:20 ~packing:scrolled_window#add
- ~share_id_to_uris_with:inputt ()
+ ~share_environment_with:inputt ()
~isnotempty_callback:
(function b ->
(*non_empty_type := b ;*)
GBin.scrolled_window ~border_width:5
~packing:(vbox#pack ~expand:true ~padding:0) () in
let newinputt =
- TexTermEditor'.term_editor
+ TermEditor'.term_editor
mqi_handle
~width:400 ~height:20 ~packing:scrolled_window#add
- ~share_id_to_uris_with:inputt ()
+ ~share_environment_with:inputt ()
~isnotempty_callback:
(function b ->
(* (*non_empty_type := b ;*)
let obj = Cic.InductiveDefinition(tys,params,!paramsno) in
begin
try
- prerr_endline (CicPp.ppobj obj) ;
+ debug_print (CicPp.ppobj obj);
CicTypeChecker.typecheck_mutual_inductive_defs uri
(tys,params,!paramsno) ;
with
e ->
- prerr_endline "Offending mutual (co)inductive type declaration:" ;
- prerr_endline (CicPp.ppobj obj) ;
+ debug_print "Offending mutual (co)inductive type declaration:" ;
+ debug_print (CicPp.ppobj obj) ;
end ;
(* We already know that obj is well-typed. We need to add it to the *)
(* environment in order to compute the inner-types without having to *)
~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
(* moved here to have visibility of the ok button *)
let newinputt =
- TexTermEditor'.term_editor
+ TermEditor'.term_editor
mqi_handle
~width:400 ~height:100 ~packing:scrolled_window#add
- ~share_id_to_uris_with:inputt ()
+ ~share_environment_with:inputt ()
~isnotempty_callback:
(function b ->
non_empty_type := b ;
okb#misc#set_sensitive (b && uri_entry#text <> ""))
in
let _ =
-let xxx = inputt#get_as_string in
-prerr_endline ("######################## " ^ xxx) ;
- newinputt#set_term xxx ;
-(*
- newinputt#set_term inputt#get_as_string ;
-*)
+ newinputt#set_term inputt#get_as_string ;
inputt#reset in
let _ =
uri_entry#connect#changed
let choose_selection mmlwidget (element : Gdome.element option) =
let module G = Gdome in
- prerr_endline "Il bandolo" ;
let rec aux element =
if element#hasAttributeNS
~namespaceURI:Misc.helmns
| Some p -> aux (new Gdome.element_of_node p)
with
GdomeInit.DOMCastException _ ->
- prerr_endline
+ debug_print
"******* trying to select above the document root ********"
in
match element with
let _ =
factory3#add_item "Edit Aliases..." ~key:GdkKeysyms._A
~callback:edit_aliases in
+ let _ =
+ factory3#add_item "Clear Aliases" ~key:GdkKeysyms._K
+ ~callback:clear_aliases in
+ let autoitem =
+ factory3#add_check_item "Auto disambiguation"
+ ~callback:(fun checked -> auto_disambiguation := checked) in
let _ = factory3#add_separator () in
let _ =
factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P
factory3#add_item "Reload Stylesheets"
~callback:
(function _ ->
- ApplyStylesheets.reload_stylesheets () ;
+ ChosenTransformer.reload_stylesheets () ;
if ProofEngine.get_proof () <> None then
try
refresh_goals notebook ;
GBin.scrolled_window ~border_width:5
~packing:frame#add () in
let inputt =
- TexTermEditor'.term_editor
+ TermEditor'.term_editor
mqi_handle
~width:400 ~height:100 ~packing:scrolled_window1#add ()
~isnotempty_callback:
GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
in
let outputhtml =
- new Ui_logger.html_logger
- ~width:400 ~height: 100
- ~packing:frame#add
- ~show:true () in
+ new Ui_logger.html_logger
+ ~width:400 ~height: 100 ~show:true ~packing:frame#add ()
+ in
object
method outputhtml = outputhtml
method inputt = inputt
method scratch_window = scratch_window
method notebook = notebook
method show = window#show
+ method set_auto_disambiguation set = autoitem#set_active set
initializer
notebook#set_empty_page ;
(*export_to_postscript_menu_item#misc#set_sensitive false ;*)
let output = TermViewer.proof_viewer ~width:350 ~height:280 () in
let notebook = new notebook in
let rendering_window' = new rendering_window output notebook in
+ rendering_window'#set_auto_disambiguation !auto_disambiguation;
set_rendering_window rendering_window' ;
let print_error_as_html prefix msg =
output_html (outputhtml ()) (`Error (`T (prefix ^ msg)))
projects / helm.git / blobdiff