Not_found -> "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm"
;;
-let empty_id_to_uris = ([],function _ -> None);;
-
-
(* GLOBAL REFERENCES (USED BY CALLBACKS) *)
let htmlheader_and_content = ref htmlheader;;
let current_goal_infos = ref None;;
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);;
let expr =
let term =
term_of_cic_textual_parser_uri
- (Disambiguate.cic_textual_parser_uri_of_string uri)
+ (Misc.cic_textual_parser_uri_of_string uri)
in
(Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term))
in
;;
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 window =
GWindow.window
let n' = Str.search_forward regexpr inputtext n in
let id = Str.matched_group 2 inputtext in
let uri =
- Disambiguate.cic_textual_parser_uri_of_string
+ Misc.cic_textual_parser_uri_of_string
("cic:" ^ (Str.matched_group 5 inputtext))
in
let dom,resolve_id = aux (n' + 1) in
id::dom,
(function id' -> if id = id' then Some uri else resolve_id id')
with
- Not_found -> empty_id_to_uris
+ Not_found -> TermEditor.empty_id_to_uris
in
aux 0
in
- id_to_uris := dom,resolve_id
+ id_to_uris := (dom,resolve_id)
;;
let proveit () =
let uris =
List.map
(function uri,_ ->
- Disambiguate.wrong_xpointer_format_from_wrong_xpointer_format' uri)
+ Misc.wrong_xpointer_format_from_wrong_xpointer_format' uri)
result in
let html =
(" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>")
end
;;
-module Disambiguate' = Disambiguate.Make(Callbacks);;
-
-class term_editor ?packing ?width ?height ?isnotempty_callback () =
- let input = GEdit.text ~editable:true ?width ?height ?packing () in
- let _ =
- match isnotempty_callback with
- None -> ()
- | Some callback ->
- ignore(input#connect#changed (function () -> callback (input#length > 0)))
- in
-object(self)
- method coerce = input#coerce
- method reset =
- input#delete_text 0 input#length
- (* CSC: txt is now a string, but should be of type Cic.term *)
- method set_term txt =
- self#reset ;
- ignore ((input#insert_text txt) ~pos:0)
- (* CSC: this method should disappear *)
- method get_as_string =
- input#get_chars 0 input#length
- method get_metasenv_and_term ~context ~metasenv =
- let name_context =
- List.map
- (function
- Some (n,_) -> Some n
- | None -> None
- ) context
- in
- let lexbuf = Lexing.from_string (input#get_chars 0 input#length) in
- let dom,mk_metasenv_and_expr =
- CicTextualParserContext.main
- ~context:name_context ~metasenv CicTextualLexer.token lexbuf
- in
- let id_to_uris',metasenv,expr =
- Disambiguate'.disambiguate_input context metasenv dom mk_metasenv_and_expr
- ~id_to_uris:!id_to_uris
- in
- id_to_uris := id_to_uris' ;
- metasenv,expr
-end
-;;
+module TermEditor' = TermEditor.Make(Callbacks);;
(* OTHER FUNCTIONS *)
let locate () =
- let inputt = ((rendering_window ())#inputt : term_editor) in
+ let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
try
match
exception NotAUriToAConstant;;
let new_inductive () =
+ let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
let notebook = (rendering_window ())#notebook in
GBin.scrolled_window ~border_width:5
~packing:(vbox#pack ~expand:true ~padding:0) () in
let newinputt =
- new term_editor ~width:400 ~height:20 ~packing:scrolled_window#add ()
+ TermEditor'.term_editor
+ ~width:400 ~height:20 ~packing:scrolled_window#add
+ ~share_id_to_uris_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 =
- new term_editor ~width:400 ~height:20 ~packing:scrolled_window#add ()
+ TermEditor'.term_editor
+ ~width:400 ~height:20 ~packing:scrolled_window#add
+ ~share_id_to_uris_with:inputt ()
~isnotempty_callback:
(function b ->
(* (*non_empty_type := b ;*)
;;
let new_proof () =
- let inputt = ((rendering_window ())#inputt : term_editor) in
+ let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
let notebook = (rendering_window ())#notebook in
~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
(* moved here to have visibility of the ok button *)
let newinputt =
- new term_editor ~width:400 ~height:100 ~packing:scrolled_window#add ()
+ TermEditor'.term_editor ~width:400 ~height:100 ~packing:scrolled_window#add
+ ~share_id_to_uris_with:inputt ()
~isnotempty_callback:
(function b ->
non_empty_type := b ;
;;
let check scratch_window () =
- let inputt = ((rendering_window ())#inputt : term_editor) in
+ let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
let metasenv =
match !ProofEngine.proof with
let module U = UriManager in
List.map
(function uri ->
- match Disambiguate.cic_textual_parser_uri_of_string uri with
+ match Misc.cic_textual_parser_uri_of_string uri with
CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[])
| _ -> assert false)
(interactive_user_uri_choice
let notebook = (rendering_window ())#notebook in
let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let inputt = ((rendering_window ())#inputt : term_editor) in
+ let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
let savedproof = !ProofEngine.proof in
let savedgoal = !ProofEngine.goal in
let uri,metasenv,bo,ty =
let notebook = (rendering_window ())#notebook in
let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let inputt = ((rendering_window ())#inputt : term_editor) in
+ let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
let savedproof = !ProofEngine.proof in
let savedgoal = !ProofEngine.goal in
match notebook#proofw#get_selections with
(fun ~row ~column ~event ->
let (uristr,_) = List.nth results row in
match
- Disambiguate.cic_textual_parser_uri_of_string
- (Disambiguate.wrong_xpointer_format_from_wrong_xpointer_format'
+ Misc.cic_textual_parser_uri_of_string
+ (Misc.wrong_xpointer_format_from_wrong_xpointer_format'
uristr)
with
CicTextualParser0.ConUri uri
;;
let completeSearchPattern () =
- let inputt = ((rendering_window ())#inputt : term_editor) in
+ let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
try
let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
;;
let searchPattern () =
- let inputt = ((rendering_window ())#inputt : term_editor) in
+ let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
try
let metasenv =
let uris =
List.map
(function uri,_ ->
- Disambiguate.wrong_xpointer_format_from_wrong_xpointer_format' uri
+ Misc.wrong_xpointer_format_from_wrong_xpointer_format' uri
) result in
let html =
" <h1>Backward Query: </h1>" ^
if
ProofEngine.can_apply
(term_of_cic_textual_parser_uri
- (Disambiguate.cic_textual_parser_uri_of_string uri))
+ (Misc.cic_textual_parser_uri_of_string uri))
then
uri::tl',exc
else
GBin.scrolled_window ~border_width:5
~packing:frame#add () in
let inputt =
- new term_editor ~width:400 ~height:100 ~packing:scrolled_window1#add ()
+ TermEditor'.term_editor
+ ~width:400 ~height:100 ~packing:scrolled_window1#add ()
~isnotempty_callback:
(function b ->
check_menu_item#misc#set_sensitive b ;
projects / helm.git / blobdiff