X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=83d959ca38f77f4ed8b76ca31a24611a50971eba;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=3c37b3ed268b67e2a57d62b00902cd8608b67d95;hpb=d7a329578a475af98aa5f2a16d9873a576dab599;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 3c37b3ed2..83d959ca3 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -33,6 +33,18 @@ (* *) (******************************************************************************) + +(* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *) +let wrong_xpointer_format_from_wrong_xpointer_format' uri = + try + let index_sharp = String.index uri '#' in + let index_rest = index_sharp + 10 in + let baseuri = String.sub uri 0 index_sharp in + let rest = String.sub uri index_rest (String.length uri - index_rest - 1) in + baseuri ^ "#" ^ rest + with Not_found -> uri +;; + (* GLOBAL CONSTANTS *) let helmns = Gdome.domString "http://www.cs.unibo.it/helm";; @@ -47,8 +59,14 @@ let htmlfooter = "" ;; +(* +let prooffile = "/home/tassi/miohelm/tmp/currentproof";; +*) let prooffile = "/public/sacerdot/currentproof";; (*CSC: the getter should handle the innertypes, not the FS *) +(* +let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";; +*) let innertypesfile = "/public/sacerdot/innertypes";; (* GLOBAL REFERENCES (USED BY CALLBACKS) *) @@ -684,8 +702,8 @@ let clear rendering_window = let fourier rendering_window = call_tactic ProofEngine.fourier rendering_window ;; -let rewrite rendering_window = - call_tactic_with_input ProofEngine.rewrite rendering_window +let rewritesimpl rendering_window = + call_tactic_with_input ProofEngine.rewrite_simpl rendering_window ;; @@ -746,7 +764,7 @@ let qed rendering_window () = (*???? let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";; *) -let dtdname = "/projects/helm/V7/dtd/cic.dtd";; +let dtdname = "/home/tassi/miohelm/helm/dtd/cic.dtd";; let save rendering_window () = let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in @@ -1108,6 +1126,14 @@ let user_uri_choice uris = String.sub uri 4 (String.length uri - 4) ;; +(* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *) +let get_last_query = + let query = ref "" in + MQueryGenerator.set_confirm_query + (function q -> query := MQueryUtil.text_of_query q ; true) ; + function result -> !query ^ "

Result:

" ^ MQueryUtil.text_of_result result "
" +;; + let locate rendering_window () = let inputt = (rendering_window#inputt : GEdit.text) in let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in @@ -1118,7 +1144,12 @@ let locate rendering_window () = [] -> () | head :: tail -> inputt#delete_text 0 inputlen ; - let MathQL.MQRefs uris, html = MQueryGenerator.locate head in + let result = MQueryGenerator.locate head in + let uris = + List.map + (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri) + result in + let html = ("

Locate Query: 

" ^ get_last_query result ^ "
") in output_html outputhtml html ; let uri' = user_uri_choice uris in ignore ((inputt#insert_text uri') ~pos:0) @@ -1144,9 +1175,16 @@ let backward rendering_window () = None -> () | Some metano -> let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in - let MathQL.MQRefs uris, html = - MQueryGenerator.backward metasenv ey ty level - in + let result = MQueryGenerator.backward metasenv ey ty level in + let uris = + List.map + (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri) + result in + let html = + "

Backward Query:

" ^ + "

Levels:

" ^ + MQueryGenerator.string_of_levels (MQueryGenerator.levels_of_term metasenv ey ty) "
" ^ + " 
" ^ get_last_query result ^ "
" in output_html outputhtml html ; let uri' = user_uri_choice uris in inputt#delete_text 0 inputlen ; @@ -1465,8 +1503,8 @@ class rendering_window output proofw (label : GMisc.label) = let fourierb = GButton.button ~label:"Fourier" ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let rewriteb = - GButton.button ~label:"Rewrite" + let rewritesimplb = + GButton.button ~label:"RewriteSimpl ->" ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in let outputhtml = GHtml.xmhtml @@ -1522,7 +1560,7 @@ object(self) ignore(clearbodyb#connect#clicked (clearbody self)) ; ignore(clearb#connect#clicked (clear self)) ; ignore(fourierb#connect#clicked (fourier self)) ; - ignore(rewriteb#connect#clicked (rewrite self)) ; + ignore(rewritesimplb#connect#clicked (rewritesimpl self)) ; ignore(introsb#connect#clicked (intros self)) ; Logger.log_callback := (Logger.log_to_html ~print_and_flush:(output_html outputhtml)) @@ -1534,7 +1572,7 @@ let rendering_window = ref None;; let initialize_everything () = let module U = Unix in - let output = GMathView.math_view ~width:400 ~height:280 () + let output = GMathView.math_view ~width:350 ~height:280 () and proofw = GMathView.math_view ~width:400 ~height:275 () and label = GMisc.label ~text:"gTopLevel" () in let rendering_window' = @@ -1549,10 +1587,15 @@ let _ = CicCooking.init () ; if !usedb then begin - MQueryGenerator.init () ; + Mqint.init "host=mowgli.cs.unibo.it dbname=helm user=helm" ; CicTextualParser0.set_locate_object (function id -> - let MathQL.MQRefs uris, html = MQueryGenerator.locate id in + let result = MQueryGenerator.locate id in + let uris = + List.map + (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri) + result in + let html = ("

Locate Query: 

" ^ get_last_query result ^ "
") in begin match !rendering_window with None -> assert false @@ -1606,5 +1649,5 @@ let _ = end ; ignore (GtkMain.Main.init ()) ; initialize_everything () ; - if !usedb then MQueryGenerator.close (); + if !usedb then Mqint.close (); ;;