-(* 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
ignore (cancelb#connect#clicked window#destroy) ;
ignore
(okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
- let dom,resolve_id = !id_to_uris in
+ let resolve_id = !id_to_uris in
ignore
(input#buffer#insert ~iter:(input#buffer#get_iter_at_char 0)
- (String.concat "\n"
- (List.map
+ (Disambiguate_types.Environment.fold
+ (fun i v s ->
+ match i with
+ | Disambiguate_types.Id id -> s ^ sprintf "alias %s %s\n" id (fst v)
+ | _ -> "")
+ resolve_id "")) ;
+(*
(function v ->
let uri =
match resolve_id v with
(* CSC: To be implemented *)
assert false
)^ " " ^ (string_of_cic_textual_parser_uri uri)
- ) dom))) ;
+ )
+*)
window#show () ;
GtkThread.main ();
if !chosen then
- let dom,resolve_id =
+ let resolve_id =
let inputtext = input#buffer#get_text () in
let regexpr =
let alfa = "[a-zA-Z_-]" 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
+ let id = Disambiguate_types.Id (Str.matched_group 2 inputtext) in
+ let uri = "cic:" ^ (Str.matched_group 5 inputtext) in
+ let resolve_id = aux (n' + 1) in
+ if Disambiguate_types.Environment.mem id resolve_id then
+ resolve_id
else
- id::dom,
- (function id' ->
- if id = id' then
- Some (CicTextualParser0.Uri uri)
- else resolve_id id')
+ let term = Disambiguate.term_of_uri uri in
+ (Disambiguate_types.Environment.add id (uri, (fun _ _ _ -> term))
+ resolve_id)
with
Not_found -> TermEditor.empty_id_to_uris
in
aux 0
in
- id_to_uris := (dom,resolve_id)
+ id_to_uris := resolve_id
;;
let proveit () =
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 =
struct
in
let _ =
let xxx = inputt#get_as_string in
-prerr_endline ("######################## " ^ xxx) ;
newinputt#set_term xxx ;
(*
newinputt#set_term inputt#get_as_string ;
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
factory3#add_item "Reload Stylesheets"
~callback:
(function _ ->
- ApplyStylesheets.reload_stylesheets () ;
+ ChosenTransformer.reload_stylesheets () ;
if ProofEngine.get_proof () <> None then
try
refresh_goals notebook ;
(* *)
(******************************************************************************)
+open Printf
+
+open Disambiguate_types
+
(* A WIDGET TO ENTER CIC TERMS *)
class type term_editor =
method reset : unit
(* The input of set_term is unquoted *)
method set_term : string -> unit
- method id_to_uris : Disambiguate.domain_and_interpretation ref
+ method id_to_uris : environment ref
end
-;;
-let empty_id_to_uris = ([],function _ -> None);;
+let empty_id_to_uris = Environment.empty
-module Make(C:Disambiguate.Callbacks) =
+module Make(C: Callbacks) =
struct
module Disambiguate' = Disambiguate.Make(C);;
- class term_editor_impl mqi_handle ?packing ?width ?height ?isnotempty_callback
- ?share_id_to_uris_with () : term_editor
+ class term_editor_impl mqi_handle ?packing ?width ?height
+ ?isnotempty_callback ?share_id_to_uris_with () : term_editor
=
let id_to_uris =
match share_id_to_uris_with with
(function () -> callback (input#buffer#char_count > 0)))
in
object(self)
+
method coerce = input#coerce
+
method reset =
input#buffer#delete input#buffer#start_iter input#buffer#end_iter
(* CSC: txt is now a string, but should be of type Cic.term *)
+
method set_term txt =
self#reset ;
ignore (input#buffer#insert txt)
+
(* CSC: this method should disappear *)
(* get_as_string returns the unquoted string *)
- method get_as_string =
- input#buffer#get_text ()
+ method get_as_string = input#buffer#get_text ()
+
method get_metasenv_and_term ~context ~metasenv =
let name_context =
List.map
| None -> None
) context
in
- let lexbuf = Lexing.from_string (input#buffer#get_text ()) 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 mqi_handle
- context metasenv dom mk_metasenv_and_expr ~id_to_uris:!id_to_uris
- in
- id_to_uris := id_to_uris' ;
- metasenv,expr
+ let term =
+ Parser.parse_term (Stream.of_string (input#buffer#get_text ()))
+ in
+ let id_to_uris',metasenv,expr =
+ Disambiguate'.disambiguate_term mqi_handle context metasenv term
+ ~aliases:!id_to_uris
+ in
+ id_to_uris := id_to_uris';
+ (metasenv, expr)
+
method id_to_uris = id_to_uris
end
let term_editor = new term_editor_impl
end
-;;
+
projects / helm.git / commitdiff