From 956b8e8dbccedb7d66ce37c4b21eb82281443f5a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 18 Nov 2002 15:24:33 +0000 Subject: [PATCH] Code clean-up: the widget in the lower-left corner is now a widget to input CIC terms, featuring the following methods: * get_term * set_term (issue: what should be its type? So far the input is a string) * reset --- helm/gTopLevel/gTopLevel.ml | 177 ++++++++++++++++-------------------- 1 file changed, 79 insertions(+), 98 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 43d8ddf15..7efc515fa 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -150,6 +150,22 @@ let argspec = in Arg.parse argspec ignore "" +(* A WIDGET TO ENTER CIC TERMS *) + +class term_editor ?packing ?width ?height () = + let input = GEdit.text ~editable:true ?width ?height ?packing () in +object(self) + method coerce = input#coerce + method reset = + input#delete_text 0 input#length + method set_term txt = + self#reset ; + ignore ((input#insert_text txt) ~pos:0) + method get_term ~context ~metasenv = + let lexbuf = Lexing.from_string (input#get_chars 0 input#length) in + CicTextualParserContext.main ~context ~metasenv CicTextualLexer.token lexbuf +end +;; (* MISC FUNCTIONS *) @@ -1052,7 +1068,7 @@ let locate_callback id = ;; let locate () = - let inputt = ((rendering_window ())#inputt : GEdit.text) in + let inputt = ((rendering_window ())#inputt : term_editor) in let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in try match @@ -1061,8 +1077,7 @@ let locate () = None -> raise NoChoice | Some input -> let uri = locate_callback input in - inputt#delete_text 0 inputt#length ; - ignore ((inputt#insert_text uri) ~pos:0) + inputt#set_term uri with e -> output_html outputhtml @@ -1294,42 +1309,37 @@ let disambiguate_input context metasenv dom mk_metasenv_and_expr = ;; let state () = - let inputt = ((rendering_window ())#inputt : GEdit.text) in + let inputt = ((rendering_window ())#inputt : term_editor) in let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in let output = ((rendering_window ())#output : GMathView.math_view) in let notebook = (rendering_window ())#notebook in - let inputlen = inputt#length in - let input = inputt#get_chars 0 inputlen ^ "\n" in - (* Do something interesting *) - let lexbuf = Lexing.from_string input in - try - let dom,mk_metasenv_and_expr = - CicTextualParserContext.main [] [] CicTextualLexer.token lexbuf - in - let metasenv,expr = - disambiguate_input [] [] dom mk_metasenv_and_expr - in - let _ = CicTypeChecker.type_of_aux' metasenv [] expr in - ProofEngine.proof := - Some (UriManager.uri_of_string "cic:/dummy.con", - (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ; - ProofEngine.goal := Some 1 ; - refresh_sequent notebook ; - refresh_proof output ; - !save_set_sensitive true ; - inputt#delete_text 0 inputlen - with - RefreshSequentException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "

") - | RefreshProofException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e ^ "

") - | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") ; + try + let dom,mk_metasenv_and_expr = inputt#get_term [] [] in + let metasenv,expr = + disambiguate_input [] [] dom mk_metasenv_and_expr + in + let _ = CicTypeChecker.type_of_aux' metasenv [] expr in + ProofEngine.proof := + Some + (UriManager.uri_of_string "cic:/dummy.con", + (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ; + ProofEngine.goal := Some 1 ; + refresh_sequent notebook ; + refresh_proof output ; + !save_set_sensitive true ; + inputt#reset + with + RefreshSequentException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") + | RefreshProofException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; ;; let check_term_in_scratch scratch_window metasenv context expr = @@ -1346,14 +1356,12 @@ prerr_endline ("### " ^ CicPp.ppterm expr ^ " ==> " ^ CicPp.ppterm ty) ; ;; let check scratch_window () = - let inputt = ((rendering_window ())#inputt : GEdit.text) in + let inputt = ((rendering_window ())#inputt : term_editor) in let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in - let inputlen = inputt#length in - let input = inputt#get_chars 0 inputlen ^ "\n" in - let curi,metasenv = + let metasenv = match !ProofEngine.proof with - None -> UriManager.uri_of_string "cic:/dummy.con", [] - | Some (curi,metasenv,_,_) -> curi,metasenv + None -> [] + | Some (_,metasenv,_,_) -> metasenv in let context,names_context = let context = @@ -1372,20 +1380,16 @@ let check scratch_window () = | None -> None ) context in - let lexbuf = Lexing.from_string input in - try - let dom,mk_metasenv_and_expr = - CicTextualParserContext.main names_context metasenv CicTextualLexer.token - lexbuf + try + let dom,mk_metasenv_and_expr = inputt#get_term names_context metasenv in + let (metasenv',expr) = + disambiguate_input context metasenv dom mk_metasenv_and_expr in - let (metasenv',expr) = - disambiguate_input context metasenv dom mk_metasenv_and_expr - in - check_term_in_scratch scratch_window metasenv' context expr - with - e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") ; + check_term_in_scratch scratch_window metasenv' context expr + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; ;; @@ -1432,23 +1436,14 @@ let call_tactic_with_input tactic () = let notebook = (rendering_window ())#notebook in let output = ((rendering_window ())#output : GMathView.math_view) in let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in - let inputt = ((rendering_window ())#inputt : GEdit.text) in + let inputt = ((rendering_window ())#inputt : term_editor) in let savedproof = !ProofEngine.proof in let savedgoal = !ProofEngine.goal in -(*CSC: Gran cut&paste da sotto... *) - let inputlen = inputt#length in - let input = inputt#get_chars 0 inputlen ^ "\n" in - let lexbuf = Lexing.from_string input in - let curi = - match !ProofEngine.proof with - None -> assert false - | Some (curi,_,_,_) -> curi - in - let uri,metasenv,bo,ty = - match !ProofEngine.proof with - None -> assert false - | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty - in + let uri,metasenv,bo,ty = + match !ProofEngine.proof with + None -> assert false + | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty + in let canonical_context = match !ProofEngine.goal with None -> assert false @@ -1466,9 +1461,7 @@ let call_tactic_with_input tactic () = ) canonical_context in try - let dom,mk_metasenv_and_expr = - CicTextualParserContext.main context metasenv CicTextualLexer.token lexbuf - in + let dom,mk_metasenv_and_expr = inputt#get_term context metasenv in let (metasenv',expr) = disambiguate_input canonical_context metasenv dom mk_metasenv_and_expr in @@ -1476,7 +1469,7 @@ let call_tactic_with_input tactic () = tactic expr ; refresh_sequent notebook ; refresh_proof output ; - inputt#delete_text 0 inputlen + inputt#reset with RefreshSequentException e -> output_html outputhtml @@ -1559,7 +1552,7 @@ let call_tactic_with_input_and_goal_input tactic () = let notebook = (rendering_window ())#notebook in let output = ((rendering_window ())#output : GMathView.math_view) in let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in - let inputt = ((rendering_window ())#inputt : GEdit.text) in + let inputt = ((rendering_window ())#inputt : term_editor) in let savedproof = !ProofEngine.proof in let savedgoal = !ProofEngine.goal in match notebook#proofw#get_selection with @@ -1576,20 +1569,11 @@ let call_tactic_with_input_and_goal_input tactic () = match !current_goal_infos with Some (ids_to_terms, ids_to_father_ids,_) -> let id = xpath in - (* Let's parse the input *) - let inputlen = inputt#length in - let input = inputt#get_chars 0 inputlen ^ "\n" in - let lexbuf = Lexing.from_string input in - let curi = - match !ProofEngine.proof with - None -> assert false - | Some (curi,_,_,_) -> curi - in - let uri,metasenv,bo,ty = - match !ProofEngine.proof with - None -> assert false - | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty - in + let uri,metasenv,bo,ty = + match !ProofEngine.proof with + None -> assert false + | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty + in let canonical_context = match !ProofEngine.goal with None -> assert false @@ -1605,9 +1589,7 @@ let call_tactic_with_input_and_goal_input tactic () = | None -> None ) canonical_context in - let dom,mk_metasenv_and_expr = - CicTextualParserContext.main context metasenv - CicTextualLexer.token lexbuf + let dom,mk_metasenv_and_expr = inputt#get_term context metasenv in let (metasenv',expr) = disambiguate_input canonical_context metasenv dom @@ -1618,7 +1600,7 @@ let call_tactic_with_input_and_goal_input tactic () = ~input:expr ; refresh_sequent notebook ; refresh_proof output ; - inputt#delete_text 0 inputlen + inputt#reset | None -> assert false (* "ERROR: No current term!!!" *) with RefreshSequentException e -> @@ -1830,7 +1812,7 @@ let open_ () = let searchPattern () = - let inputt = ((rendering_window ())#inputt : GEdit.text) in + let inputt = ((rendering_window ())#inputt : term_editor) in let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in try let rec get_level ?(last_invalid=false) () = @@ -1914,8 +1896,7 @@ let searchPattern () = "Many lemmas can be successfully applied. Please, choose one:" uris' in - inputt#delete_text 0 inputt#length ; - ignore ((inputt#insert_text uri') ~pos:0) ; + inputt#set_term uri' ; apply () with e -> @@ -2422,8 +2403,8 @@ class rendering_window output (notebook : notebook) = let scrolled_window1 = GBin.scrolled_window ~border_width:5 ~packing:(vbox'#pack ~expand:true ~padding:0) () in - let inputt = GEdit.text ~editable:true ~width:400 ~height:100 - ~packing:scrolled_window1#add () in + let inputt = + new term_editor ~width:400 ~height:100 ~packing:scrolled_window1#add () in let vboxl = GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in let _ = -- 2.39.2