let uri =
match resolve_id v with
None -> assert false
- | Some uri -> uri
+ | Some (CicTextualParser0.Uri uri) -> uri
+ | Some (CicTextualParser0.Term _)
+ | Some CicTextualParser0.Implicit -> assert false
in
- "alias " ^ v ^ " " ^
- (string_of_cic_textual_parser_uri uri)
+ "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))) ;
window#show () ;
GtkThread.main ();
let rec aux n =
try
let n' = Str.search_forward regexpr inputtext n in
- let id = Str.matched_group 2 inputtext 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))
dom,resolve_id
else
id::dom,
- (function id' -> if id = id' then Some uri else resolve_id id')
+ (function id' ->
+ if id = id' then
+ Some (CicTextualParser0.Uri uri)
+ else resolve_id id')
with
Not_found -> TermEditor.empty_id_to_uris
in
let obj = CicEnvironment.get_obj uri in
show_in_show_window_obj uri obj
in
- let show_in_show_window_callback mmlwidget (n : Gdome.element) _ =
- if n#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then
- let uri =
- (n#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string
- in
- show_in_show_window_uri (UriManager.uri_of_string uri)
- else
- ignore (mmlwidget#action_toggle n)
+ let show_in_show_window_callback mmlwidget (n : Gdome.element option) _ =
+ match n with
+ None -> ()
+ | Some n' ->
+ if n'#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then
+ let uri =
+ (n'#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string
+ in
+ show_in_show_window_uri (UriManager.uri_of_string uri)
+ else
+ ignore (mmlwidget#action_toggle n')
in
let _ =
mmlwidget#connect#click (show_in_show_window_callback mmlwidget)
(* A WIDGET TO ENTER CIC TERMS *)
+module ChosenTermEditor = TexTermEditor;;
+module ChosenTextualParser0 = TexCicTextualParser0;;
+(*
+module ChosenTermEditor = TermEditor;;
+module ChosenTextualParser0 = CicTextualParser0;;
+*)
+
module Callbacks =
struct
+ let get_metasenv () = !ChosenTextualParser0.metasenv
+ let set_metasenv metasenv = ChosenTextualParser0.metasenv := metasenv
+
let output_html msg = output_html (outputhtml ()) msg;;
let interactive_user_uri_choice =
fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id ->
end
;;
-module Disambiguate' = Disambiguate.Make(Callbacks);;
-
-module TermEditor' = TermEditor.Make(Callbacks);;
+module TexTermEditor' = ChosenTermEditor.Make(Callbacks);;
(* OTHER FUNCTIONS *)
GBin.scrolled_window ~border_width:5
~packing:(vbox#pack ~expand:true ~padding:0) () in
let newinputt =
- TermEditor'.term_editor
+ TexTermEditor'.term_editor
~width:400 ~height:20 ~packing:scrolled_window#add
~share_id_to_uris_with:inputt ()
~isnotempty_callback:
GBin.scrolled_window ~border_width:5
~packing:(vbox#pack ~expand:true ~padding:0) () in
let newinputt =
- TermEditor'.term_editor
+ TexTermEditor'.term_editor
~width:400 ~height:20 ~packing:scrolled_window#add
~share_id_to_uris_with:inputt ()
~isnotempty_callback:
~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
(* moved here to have visibility of the ok button *)
let newinputt =
- TermEditor'.term_editor ~width:400 ~height:100 ~packing:scrolled_window#add
+ TexTermEditor'.term_editor ~width:400 ~height:100 ~packing:scrolled_window#add
~share_id_to_uris_with:inputt ()
~isnotempty_callback:
(function b ->
factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show
in
let insert_query_item =
- factory4#add_item "Insert Query (Experts Only)..." ~key:GdkKeysyms._U
+ factory4#add_item "Insert Query (Experts Only)..." ~key:GdkKeysyms._Y
~callback:insertQuery in
(* hbugs menu *)
let hbugs_menu = factory0#add_submenu "HBugs" in
GBin.scrolled_window ~border_width:5
~packing:frame#add () in
let inputt =
- TermEditor'.term_editor
+ TexTermEditor'.term_editor
~width:400 ~height:100 ~packing:scrolled_window1#add ()
~isnotempty_callback:
(function b ->