let getterURL = Configuration.getter_url;;
let processorURL = Configuration.processor_url;;
-(*
-let processorURL = "http://phd.cs.unibo.it:8080/helm/servelt/uwobo/";;
-let getterURL = "http://phd.cs.unibo.it:8081/";;
-let processorURL = "http://localhost:8080/helm/servelt/uwobo/";;
-let getterURL = "http://localhost:8081/";;
-*)
let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
let mml_args =
(*CSC: We save the innertypes to disk so that we can retrieve them in the *)
(*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
(*CSC: local. *)
- Xml.pp xmlinnertypes (Some "/public/sacerdot/innertypes") ;
+ Xml.pp xmlinnertypes (Some "/public/fguidi/innertypes") ;
let output = applyStylesheets input mml_styles mml_args in
output
;;
output_html outputhtml
("<h1 color=\"red\">Exception raised during the refresh of the " ^
"proof: " ^ Printexc.to_string e ^ "</h1>") ;
-prerr_endline "PROVA CHE FA SOLLEVARE UN'ECCEZIONE:" ; flush stderr ;
-begin
-match !ProofEngine.proof with Some (_,metasenv,bo,_) ->
-List.iter (function (i,ty) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^
-CicPp.ppterm ty) ; flush stderr) metasenv ;
-prerr_endline ("PROOF: " ^ CicPp.ppterm bo) ; flush stderr ;
-end ;
ProofEngine.proof := savedproof ;
ProofEngine.goal := savedgoal ;
refresh_sequent proofw ;
match !ProofEngine.proof with
None -> assert false
| Some (uri,[],bo,ty) ->
- if CicReduction.are_convertible (CicTypeChecker.type_of_aux' [] [] bo) ty then
+ if
+ CicReduction.are_convertible []
+ (CicTypeChecker.type_of_aux' [] [] bo) ty
+ then
begin
(*CSC: Wrong: [] is just plainly wrong *)
let proof = Cic.Definition (UriManager.name_of_uri uri,bo,ty,[]) in
refresh_sequent rendering_window#proofw
| None -> assert false (* "ERROR: No current term!!!" *)
with
- e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ RefreshSequentException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>")
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
end
| None -> assert false (* "ERROR: No selection!!!" *)
;;
ProofEngine.proof :=
Some (uri, metasenv, bo, ty) ;
ProofEngine.goal := None ;
- inputt#delete_text 0 inputlen ;
- ignore(oldinputt#insert_text input oldinputt#length) ;
refresh_sequent proofw ;
refresh_proof output ;
+ inputt#delete_text 0 inputlen ;
+ ignore(oldinputt#insert_text input oldinputt#length)
with
- e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ RefreshSequentException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>")
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
;;
let state rendering_window () =
match CicTextualParser.main CicTextualLexer.token lexbuf with
None -> ()
| Some expr ->
- try
- let _ = CicTypeChecker.type_of_aux' [] [] expr in
- ProofEngine.proof :=
- Some (UriManager.uri_of_string "cic:/dummy.con",
- [1,expr], Cic.Meta 1, expr) ;
- ProofEngine.goal := Some (1,([],expr)) ;
- refresh_sequent proofw ;
- refresh_proof output ;
- with
- e ->
- print_endline ("? " ^ CicPp.ppterm expr) ;
- raise e
+ let _ = CicTypeChecker.type_of_aux' [] [] expr in
+ ProofEngine.proof :=
+ Some (UriManager.uri_of_string "cic:/dummy.con",
+ [1,expr], Cic.Meta 1, expr) ;
+ ProofEngine.goal := Some (1,([],expr)) ;
+ refresh_sequent proofw ;
+ refresh_proof output ;
done
with
CicTextualParser0.Eof ->
inputt#delete_text 0 inputlen ;
ignore(oldinputt#insert_text input oldinputt#length)
+ | RefreshSequentException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>")
| e ->
output_html outputhtml
("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
let check rendering_window scratch_window () =
let inputt = (rendering_window#inputt : GEdit.text) in
- let oldinputt = (rendering_window#oldinputt : GEdit.text) in
let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
let output = (rendering_window#output : GMathView.math_view) in
let proofw = (rendering_window#proofw : GMathView.math_view) in
raise e
done
with
- CicTextualParser0.Eof ->
- inputt#delete_text 0 inputlen ;
- ignore(oldinputt#insert_text input oldinputt#length)
+ CicTextualParser0.Eof -> ()
| e ->
output_html outputhtml
("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
;;
+let locate rendering_window () =
+ let inputt = (rendering_window#inputt : GEdit.text) in
+ let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
+ let inputlen = inputt#length in
+ let input = inputt#get_chars 0 inputlen in
+ try
+ output_html outputhtml (Mquery.locate input) ;
+ inputt#delete_text 0 inputlen
+ with
+ e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+;;
+
+let backward rendering_window () =
+ let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
+ let result =
+ match !ProofEngine.goal with
+ | None -> ""
+ | Some (_, (_, t)) -> (Mquery.backward t)
+ in
+ output_html outputhtml result
+
let choose_selection
(mmlwidget : GMathView.math_view) (element : Gdome.element option)
=
let checkb =
GButton.button ~label:"Check"
~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let locateb =
+ GButton.button ~label:"Locate"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let backwardb =
+ GButton.button ~label:"Backward"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
let inputt = GEdit.text ~editable:true ~width:400 ~height: 100
~packing:(vbox#pack ~padding:5) () in
let vbox1 =
ignore(stateb#connect#clicked (state self)) ;
ignore(openb#connect#clicked (open_ self)) ;
ignore(checkb#connect#clicked (check self scratch_window)) ;
+ ignore(locateb#connect#clicked (locate self)) ;
+ ignore(backwardb#connect#clicked (backward self)) ;
ignore(exactb#connect#clicked (exact self)) ;
ignore(applyb#connect#clicked (apply self)) ;
ignore(elimintrosb#connect#clicked (elimintros self)) ;
projects / helm.git / blobdiff