helm/gTopLevel/gTopLevel.ml

   1 (* Copyright (C) 2000-2002, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (******************************************************************************)
  27 (*                                                                            *)
  28 (*                               PROJECT HELM                                 *)
  29 (*                                                                            *)
  30 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
  31 (*                                 06/01/2002                                 *)
  32 (*                                                                            *)
  33 (*                                                                            *)
  34 (******************************************************************************)
  35
  36
  37 (* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *)
  38 let wrong_xpointer_format_from_wrong_xpointer_format' uri =
  39  try
  40   let index_sharp =  String.index uri '#' in
  41   let index_rest = index_sharp + 10 in
  42    let baseuri = String.sub uri 0 index_sharp in
  43    let rest = String.sub uri index_rest (String.length uri - index_rest - 1) in
  44     baseuri ^ "#" ^ rest
  45  with Not_found -> uri
  46 ;;
  47
  48 (* GLOBAL CONSTANTS *)
  49
  50 let helmns = Gdome.domString "http://www.cs.unibo.it/helm";;
  51 let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
  52
  53 let htmlheader =
  54  "<html>" ^
  55  " <body bgColor=\"white\">"
  56 ;;
  57
  58 let htmlfooter =
  59  " </body>" ^
  60  "</html>"
  61 ;;
  62
  63
  64 let prooffile = "/home/galata/miohelm/currentproof";;
  65 let prooffiletype = "/home/galata/miohelm/currentprooftype";;
  66
  67 (*CSC: the getter should handle the innertypes, not the FS *)
  68
  69 let innertypesfile = "/home/galata/miohelm/innertypes";;
  70 let constanttypefile = "/home/galata/miohelm/constanttype";;
  71
  72 let empty_id_to_uris = ([],function _ -> None);;
  73
  74
  75 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
  76
  77 let htmlheader_and_content = ref htmlheader;;
  78
  79 let current_cic_infos = ref None;;
  80 let current_goal_infos = ref None;;
  81 let current_scratch_infos = ref None;;
  82
  83 let id_to_uris = ref empty_id_to_uris;;
  84
  85 let check_term = ref (fun _ _ _ -> assert false);;
  86 let mml_of_cic_term_ref = ref (fun _ _ -> assert false);;
  87
  88 exception RenderingWindowsNotInitialized;;
  89
  90 let set_rendering_window,rendering_window =
  91  let rendering_window_ref = ref None in
  92   (function rw -> rendering_window_ref := Some rw),
  93   (function () ->
  94     match !rendering_window_ref with
  95        None -> raise RenderingWindowsNotInitialized
  96      | Some rw -> rw
  97   )
  98 ;;
  99
 100 exception SettingsWindowsNotInitialized;;
 101
 102 let set_settings_window,settings_window =
 103  let settings_window_ref = ref None in
 104   (function rw -> settings_window_ref := Some rw),
 105   (function () ->
 106     match !settings_window_ref with
 107        None -> raise SettingsWindowsNotInitialized
 108      | Some rw -> rw
 109   )
 110 ;;
 111
 112 exception OutputHtmlNotInitialized;;
 113
 114 let set_outputhtml,outputhtml =
 115  let outputhtml_ref = ref None in
 116   (function rw -> outputhtml_ref := Some rw),
 117   (function () ->
 118     match !outputhtml_ref with
 119        None -> raise OutputHtmlNotInitialized
 120      | Some outputhtml -> outputhtml
 121   )
 122 ;;
 123
 124 exception QedSetSensitiveNotInitialized;;
 125 let qed_set_sensitive =
 126  ref (function _ -> raise QedSetSensitiveNotInitialized)
 127 ;;
 128
 129 exception SaveSetSensitiveNotInitialized;;
 130 let save_set_sensitive =
 131  ref (function _ -> raise SaveSetSensitiveNotInitialized)
 132 ;;
 133
 134 (* COMMAND LINE OPTIONS *)
 135
 136 let usedb = ref true
 137
 138 let argspec =
 139   [
 140     "-nodb", Arg.Clear usedb, "disable use of MathQL DB"
 141   ]
 142 in
 143 Arg.parse argspec ignore ""
 144
 145 (* A WIDGET TO ENTER CIC TERMS *)
 146
 147 class term_editor ?packing ?width ?height ?isnotempty_callback () =
 148  let input = GEdit.text ~editable:true ?width ?height ?packing () in
 149  let _ =
 150   match isnotempty_callback with
 151      None -> ()
 152    | Some callback ->
 153       ignore(input#connect#changed (function () -> callback (input#length > 0)))
 154  in
 155 object(self)
 156  method coerce = input#coerce
 157  method reset =
 158   input#delete_text 0 input#length
 159  (* CSC: txt is now a string, but should be of type Cic.term *)
 160  method set_term txt =
 161   self#reset ;
 162   ignore ((input#insert_text txt) ~pos:0)
 163  (* CSC: this method should disappear *)
 164  method get_as_string =
 165   input#get_chars 0 input#length
 166  method get_term ~context ~metasenv =
 167   let lexbuf = Lexing.from_string (input#get_chars 0 input#length) in
 168    CicTextualParserContext.main ~context ~metasenv CicTextualLexer.token lexbuf
 169 end
 170 ;;
 171
 172 (* MISC FUNCTIONS *)
 173
 174 exception IllFormedUri of string;;
 175
 176 let cic_textual_parser_uri_of_string uri' =
 177  try
 178   (* Constant *)
 179   if String.sub uri' (String.length uri' - 4) 4 = ".con" then
 180    CicTextualParser0.ConUri (UriManager.uri_of_string uri')
 181   else
 182    if String.sub uri' (String.length uri' - 4) 4 = ".var" then
 183     CicTextualParser0.VarUri (UriManager.uri_of_string uri')
 184    else
 185     (try
 186       (* Inductive Type *)
 187       let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
 188        CicTextualParser0.IndTyUri (uri'',typeno)
 189      with
 190       _ ->
 191        (* Constructor of an Inductive Type *)
 192        let uri'',typeno,consno =
 193         CicTextualLexer.indconuri_of_uri uri'
 194        in
 195         CicTextualParser0.IndConUri (uri'',typeno,consno)
 196     )
 197  with
 198   _ -> raise (IllFormedUri uri')
 199 ;;
 200
 201 let term_of_cic_textual_parser_uri uri =
 202  let module C = Cic in
 203  let module CTP = CicTextualParser0 in
 204   match uri with
 205      CTP.ConUri uri -> C.Const (uri,[])
 206    | CTP.VarUri uri -> C.Var (uri,[])
 207    | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[])
 208    | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[])
 209 ;;
 210
 211 let string_of_cic_textual_parser_uri uri =
 212  let module C = Cic in
 213  let module CTP = CicTextualParser0 in
 214   let uri' =
 215    match uri with
 216       CTP.ConUri uri -> UriManager.string_of_uri uri
 217     | CTP.VarUri uri -> UriManager.string_of_uri uri
 218     | CTP.IndTyUri (uri,tyno) ->
 219        UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1)
 220     | CTP.IndConUri (uri,tyno,consno) ->
 221        UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^
 222         string_of_int consno
 223   in
 224    (* 4 = String.length "cic:" *)
 225    String.sub uri' 4 (String.length uri' - 4)
 226 ;;
 227
 228 let output_html outputhtml msg =
 229  htmlheader_and_content := !htmlheader_and_content ^ msg ;
 230  outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
 231  outputhtml#set_topline (-1)
 232 ;;
 233
 234 (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *)
 235
 236 (* Check window *)
 237
 238 let check_window outputhtml uris =
 239  let window =
 240   GWindow.window
 241    ~width:800 ~modal:true ~title:"Check" ~border_width:2 () in
 242  let notebook =
 243   GPack.notebook ~scrollable:true ~packing:window#add () in
 244  window#show () ;
 245  let render_terms =
 246   List.map
 247    (function uri ->
 248      let scrolled_window =
 249       GBin.scrolled_window ~border_width:10
 250        ~packing:
 251          (notebook#append_page ~tab_label:((GMisc.label ~text:uri ())#coerce))
 252        ()
 253      in
 254       lazy
 255        (let mmlwidget =
 256          GMathView.math_view
 257           ~packing:scrolled_window#add ~width:400 ~height:280 () in
 258         let expr =
 259          let term =
 260           term_of_cic_textual_parser_uri (cic_textual_parser_uri_of_string uri)
 261          in
 262           (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term))
 263         in
 264          try
 265           let mml = !mml_of_cic_term_ref 111 expr in
 266 prerr_endline ("### " ^ CicPp.ppterm expr) ;
 267            mmlwidget#load_tree ~dom:mml
 268          with
 269           e ->
 270            output_html outputhtml
 271             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 272        )
 273    ) uris
 274  in
 275   ignore
 276    (notebook#connect#switch_page
 277      (function i -> Lazy.force (List.nth render_terms i)))
 278 ;;
 279
 280 exception NoChoice;;
 281
 282 let
 283  interactive_user_uri_choice ~selection_mode ?(ok="Ok") ~title ~msg uris
 284 =
 285  let choices = ref [] in
 286  let chosen = ref false in
 287  let window =
 288   GWindow.dialog ~modal:true ~title ~width:600 () in
 289  let lMessage =
 290   GMisc.label ~text:msg
 291    ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
 292  let scrolled_window =
 293   GBin.scrolled_window ~border_width:10
 294    ~packing:(window#vbox#pack ~expand:true ~fill:true ~padding:5) () in
 295  let clist =
 296   let expected_height = 18 * List.length uris in
 297    let height = if expected_height > 400 then 400 else expected_height in
 298     GList.clist ~columns:1 ~packing:scrolled_window#add
 299      ~height ~selection_mode () in
 300  let _ = List.map (function x -> clist#append [x]) uris in
 301  let hbox2 =
 302   GPack.hbox ~border_width:0
 303    ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
 304  let explain_label =
 305   GMisc.label ~text:"None of the above. Try this one:"
 306    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
 307  let manual_input =
 308   GEdit.entry ~editable:true
 309    ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
 310  let hbox =
 311   GPack.hbox ~border_width:0 ~packing:window#action_area#add () in
 312  let okb =
 313   GButton.button ~label:ok
 314    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 315  let _ = okb#misc#set_sensitive false in
 316  let checkb =
 317   GButton.button ~label:"Check"
 318    ~packing:(hbox#pack ~padding:5) () in
 319  let _ = checkb#misc#set_sensitive false in
 320  let cancelb =
 321   GButton.button ~label:"Abort"
 322    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 323  (* actions *)
 324  let check_callback () =
 325   assert (List.length !choices > 0) ;
 326   check_window (outputhtml ()) !choices
 327  in
 328   ignore (window#connect#destroy GMain.Main.quit) ;
 329   ignore (cancelb#connect#clicked window#destroy) ;
 330   ignore
 331    (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
 332   ignore (checkb#connect#clicked check_callback) ;
 333   ignore
 334    (clist#connect#select_row
 335      (fun ~row ~column ~event ->
 336        checkb#misc#set_sensitive true ;
 337        okb#misc#set_sensitive true ;
 338        choices := (List.nth uris row)::!choices)) ;
 339   ignore
 340    (clist#connect#unselect_row
 341      (fun ~row ~column ~event ->
 342        choices :=
 343         List.filter (function uri -> uri != (List.nth uris row)) !choices)) ;
 344   ignore
 345    (manual_input#connect#changed
 346      (fun _ ->
 347        if manual_input#text = "" then
 348         begin
 349          choices := [] ;
 350          checkb#misc#set_sensitive false ;
 351          okb#misc#set_sensitive false ;
 352          clist#misc#set_sensitive true
 353         end
 354        else
 355         begin
 356          choices := [manual_input#text] ;
 357          clist#unselect_all () ;
 358          checkb#misc#set_sensitive true ;
 359          okb#misc#set_sensitive true ;
 360          clist#misc#set_sensitive false
 361         end));
 362   window#set_position `CENTER ;
 363   window#show () ;
 364   GMain.Main.main () ;
 365   if !chosen && List.length !choices > 0 then
 366    !choices
 367   else
 368    raise NoChoice
 369 ;;
 370
 371 let interactive_interpretation_choice interpretations =
 372  let chosen = ref None in
 373  let window =
 374   GWindow.window
 375    ~modal:true ~title:"Ambiguous well-typed input." ~border_width:2 () in
 376  let vbox = GPack.vbox ~packing:window#add () in
 377  let lMessage =
 378   GMisc.label
 379    ~text:
 380     ("Ambiguous input since there are many well-typed interpretations." ^
 381      " Please, choose one of them.")
 382    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 383  let notebook =
 384   GPack.notebook ~scrollable:true
 385    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
 386  let _ =
 387   List.map
 388    (function interpretation ->
 389      let clist =
 390       let expected_height = 18 * List.length interpretation in
 391        let height = if expected_height > 400 then 400 else expected_height in
 392         GList.clist ~columns:2 ~packing:notebook#append_page ~height
 393          ~titles:["id" ; "URI"] ()
 394      in
 395       ignore
 396        (List.map
 397          (function (id,uri) ->
 398            let n = clist#append [id;uri] in
 399             clist#set_row ~selectable:false n
 400          ) interpretation
 401        ) ;
 402       clist#columns_autosize ()
 403    ) interpretations in
 404  let hbox =
 405   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 406  let okb =
 407   GButton.button ~label:"Ok"
 408    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 409  let cancelb =
 410   GButton.button ~label:"Abort"
 411    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 412  (* actions *)
 413  ignore (window#connect#destroy GMain.Main.quit) ;
 414  ignore (cancelb#connect#clicked window#destroy) ;
 415  ignore
 416   (okb#connect#clicked
 417     (function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
 418  window#set_position `CENTER ;
 419  window#show () ;
 420  GMain.Main.main () ;
 421  match !chosen with
 422     None -> raise NoChoice
 423   | Some n -> n
 424 ;;
 425
 426
 427 (* MISC FUNCTIONS *)
 428
 429 (* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
 430 let get_last_query =
 431  let query = ref "" in
 432   MQueryGenerator.set_confirm_query
 433    (function q -> query := MQueryUtil.text_of_query q ; true) ;
 434   function result -> !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
 435 ;;
 436
 437 let domImpl = Gdome.domImplementation ();;
 438
 439 let parseStyle name =
 440  let style =
 441   domImpl#createDocumentFromURI
 442 (*
 443    ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None
 444 *)
 445    ~uri:("styles/" ^ name) ()
 446  in
 447   Gdome_xslt.processStylesheet style
 448 ;;
 449
 450 let d_c = parseStyle "drop_coercions.xsl";;
 451 let tc1 = parseStyle "objtheorycontent.xsl";;
 452 let hc2 = parseStyle "content_to_html.xsl";;
 453 let l   = parseStyle "link.xsl";;
 454
 455 let c1 = parseStyle "rootcontent.xsl";;
 456 let g  = parseStyle "genmmlid.xsl";;
 457 let c2 = parseStyle "annotatedpres.xsl";;
 458
 459
 460 let getterURL = Configuration.getter_url;;
 461 let processorURL = Configuration.processor_url;;
 462
 463 let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
 464 let mml_args ~explode_all =
 465  ("explodeall",(if explode_all then "true()" else "false()"))::
 466   ["processorURL", "'" ^ processorURL ^ "'" ;
 467    "getterURL", "'" ^ getterURL ^ "'" ;
 468    "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
 469    "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
 470    "UNICODEvsSYMBOL", "'symbol'" ;
 471    "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
 472    "encoding", "'iso-8859-1'" ;
 473    "media-type", "'text/html'" ;
 474    "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
 475    "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
 476    "naturalLanguage", "'yes'" ;
 477    "annotations", "'no'" ;
 478    "URLs_or_URIs", "'URIs'" ;
 479    "topurl", "'http://phd.cs.unibo.it/helm'" ;
 480    "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
 481 ;;
 482
 483 let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
 484 let sequent_args =
 485  ["processorURL", "'" ^ processorURL ^ "'" ;
 486   "getterURL", "'" ^ getterURL ^ "'" ;
 487   "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
 488   "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
 489   "UNICODEvsSYMBOL", "'symbol'" ;
 490   "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
 491   "encoding", "'iso-8859-1'" ;
 492   "media-type", "'text/html'" ;
 493   "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
 494   "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
 495   "naturalLanguage", "'no'" ;
 496   "annotations", "'no'" ;
 497   "explodeall", "true()" ;
 498   "URLs_or_URIs", "'URIs'" ;
 499   "topurl", "'http://phd.cs.unibo.it/helm'" ;
 500   "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
 501 ;;
 502
 503 let parse_file filename =
 504  let inch = open_in filename in
 505   let rec read_lines () =
 506    try
 507     let line = input_line inch in
 508      line ^ read_lines ()
 509    with
 510     End_of_file -> ""
 511   in
 512    read_lines ()
 513 ;;
 514
 515 let applyStylesheets input styles args =
 516  List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
 517   input styles
 518 ;;
 519
 520 let
 521  mml_of_cic_object ~explode_all uri annobj ids_to_inner_sorts ids_to_inner_types
 522 =
 523 (*CSC: ????????????????? *)
 524  let xml, bodyxml =
 525   Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:true
 526    annobj
 527  in
 528  let xmlinnertypes =
 529   Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
 530    ~ask_dtd_to_the_getter:true
 531  in
 532   let input =
 533    match bodyxml with
 534       None -> Xml2Gdome.document_of_xml domImpl xml
 535     | Some bodyxml' ->
 536        Xml.pp xml (Some constanttypefile) ;
 537        Xml2Gdome.document_of_xml domImpl bodyxml'
 538   in
 539 (*CSC: We save the innertypes to disk so that we can retrieve them in the  *)
 540 (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
 541 (*CSC: local.                                                              *)
 542    Xml.pp xmlinnertypes (Some innertypesfile) ;
 543    let output = applyStylesheets input mml_styles (mml_args ~explode_all) in
 544     output
 545 ;;
 546
 547 let
 548  save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname
 549 =
 550  let name =
 551   let struri = UriManager.string_of_uri uri in
 552   let idx = (String.rindex struri '/') + 1 in
 553    String.sub struri idx (String.length struri - idx)
 554  in
 555   let path = pathname ^ "/" ^ name in
 556   let xml, bodyxml =
 557    Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false
 558     annobj
 559   in
 560   let xmlinnertypes =
 561    Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
 562     ~ask_dtd_to_the_getter:false
 563   in
 564    (* innertypes *)
 565    let innertypesuri = UriManager.innertypesuri_of_uri uri in
 566     Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ;
 567     Getter.register innertypesuri
 568      (Configuration.annotations_url ^
 569        Str.replace_first (Str.regexp "^cic:") ""
 570         (UriManager.string_of_uri innertypesuri) ^ ".xml"
 571      ) ;
 572     (* constant type / variable / mutual inductive types definition *)
 573     Xml.pp ~quiet:true xml (Some (path ^ ".xml")) ;
 574     Getter.register uri
 575      (Configuration.annotations_url ^
 576        Str.replace_first (Str.regexp "^cic:") ""
 577         (UriManager.string_of_uri uri) ^ ".xml"
 578      ) ;
 579     match bodyxml with
 580        None -> ()
 581      | Some bodyxml' ->
 582         (* constant body *)
 583         let bodyuri =
 584          match UriManager.bodyuri_of_uri uri with
 585             None -> assert false
 586           | Some bodyuri -> bodyuri
 587         in
 588          Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ;
 589          Getter.register bodyuri
 590           (Configuration.annotations_url ^
 591             Str.replace_first (Str.regexp "^cic:") ""
 592              (UriManager.string_of_uri bodyuri) ^ ".xml"
 593           )
 594 ;;
 595
 596
 597 (* CALLBACKS *)
 598
 599 exception RefreshSequentException of exn;;
 600 exception RefreshProofException of exn;;
 601
 602 let refresh_proof (output : GMathView.math_view) =
 603  try
 604   let uri,currentproof =
 605    match !ProofEngine.proof with
 606       None -> assert false
 607     | Some (uri,metasenv,bo,ty) ->
 608        !qed_set_sensitive (List.length metasenv = 0) ;
 609        (*CSC: Wrong: [] is just plainly wrong *)
 610        uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
 611   in
 612    let
 613     (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
 614      ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
 615    =
 616     Cic2acic.acic_object_of_cic_object currentproof
 617    in
 618     let mml =
 619      mml_of_cic_object ~explode_all:true uri acic ids_to_inner_sorts
 620       ids_to_inner_types
 621     in
 622      output#load_tree mml ;
 623      current_cic_infos :=
 624       Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses)
 625  with
 626   e ->
 627  match !ProofEngine.proof with
 628     None -> assert false
 629   | Some (uri,metasenv,bo,ty) ->
 630 prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
 631    raise (RefreshProofException e)
 632 ;;
 633
 634 let refresh_sequent ?(empty_notebook=true) notebook =
 635  try
 636   match !ProofEngine.goal with
 637      None ->
 638       if empty_notebook then
 639        begin
 640         notebook#remove_all_pages ~skip_switch_page_event:false ;
 641         notebook#set_empty_page
 642        end
 643       else
 644        notebook#proofw#unload
 645    | Some metano ->
 646       let metasenv =
 647        match !ProofEngine.proof with
 648           None -> assert false
 649         | Some (_,metasenv,_,_) -> metasenv
 650       in
 651       let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
 652        let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
 653         SequentPp.XmlPp.print_sequent metasenv currentsequent
 654        in
 655         let regenerate_notebook () =
 656          let skip_switch_page_event =
 657           match metasenv with
 658              (m,_,_)::_ when m = metano -> false
 659            | _ -> true
 660          in
 661           notebook#remove_all_pages ~skip_switch_page_event ;
 662           List.iter (function (m,_,_) -> notebook#add_page m) metasenv ;
 663         in
 664           if empty_notebook then
 665            begin
 666             regenerate_notebook () ;
 667             notebook#set_current_page ~may_skip_switch_page_event:false metano
 668            end
 669           else
 670            begin
 671             let sequent_doc = Xml2Gdome.document_of_xml domImpl sequent_gdome in
 672             let sequent_mml =
 673              applyStylesheets sequent_doc sequent_styles sequent_args
 674             in
 675              notebook#set_current_page ~may_skip_switch_page_event:true metano;
 676              notebook#proofw#load_tree ~dom:sequent_mml
 677            end ;
 678           current_goal_infos :=
 679            Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
 680  with
 681   e ->
 682 let metano =
 683   match !ProofEngine.goal with
 684      None -> assert false
 685    | Some m -> m
 686 in
 687 let metasenv =
 688  match !ProofEngine.proof with
 689     None -> assert false
 690   | Some (_,metasenv,_,_) -> metasenv
 691 in
 692 try
 693 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
 694 prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
 695    raise (RefreshSequentException e)
 696 with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unkown."); raise (RefreshSequentException e)
 697 ;;
 698
 699 (*
 700 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
 701  ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ;
 702 *)
 703
 704 let mml_of_cic_term metano term =
 705  let metasenv =
 706   match !ProofEngine.proof with
 707      None -> []
 708    | Some (_,metasenv,_,_) -> metasenv
 709  in
 710  let context =
 711   match !ProofEngine.goal with
 712      None -> []
 713    | Some metano ->
 714       let (_,canonical_context,_) =
 715        List.find (function (m,_,_) -> m=metano) metasenv
 716       in
 717        canonical_context
 718  in
 719    let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
 720     SequentPp.XmlPp.print_sequent metasenv (metano,context,term)
 721    in
 722     let sequent_doc =
 723      Xml2Gdome.document_of_xml domImpl sequent_gdome
 724     in
 725      let res =
 726       applyStylesheets sequent_doc sequent_styles sequent_args ;
 727      in
 728       current_scratch_infos :=
 729        Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ;
 730       res
 731 ;;
 732
 733 exception OpenConjecturesStillThere;;
 734 exception WrongProof;;
 735
 736 let pathname_of_annuri uristring =
 737  Configuration.annotations_dir ^
 738   Str.replace_first (Str.regexp "^cic:") "" uristring
 739 ;;
 740
 741 let make_dirs dirpath =
 742  ignore (Unix.system ("mkdir -p " ^ dirpath))
 743 ;;
 744
 745 let qed () =
 746  match !ProofEngine.proof with
 747     None -> assert false
 748   | Some (uri,[],bo,ty) ->
 749      if
 750       CicReduction.are_convertible []
 751        (CicTypeChecker.type_of_aux' [] [] bo) ty
 752      then
 753       begin
 754        (*CSC: Wrong: [] is just plainly wrong *)
 755        let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in
 756         let
 757          (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
 758           ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
 759         =
 760          Cic2acic.acic_object_of_cic_object proof
 761         in
 762          let mml =
 763           mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts
 764            ids_to_inner_types
 765          in
 766           ((rendering_window ())#output : GMathView.math_view)#load_tree mml ;
 767           !qed_set_sensitive false ;
 768           (* let's save the theorem and register it to the getter *)
 769           let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
 770           make_dirs pathname ;
 771           save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
 772            pathname ;
 773           current_cic_infos :=
 774            Some
 775             (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
 776              ids_to_hypotheses)
 777       end
 778      else
 779       raise WrongProof
 780   | _ -> raise OpenConjecturesStillThere
 781 ;;
 782
 783 let save () =
 784  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
 785   match !ProofEngine.proof with
 786      None -> assert false
 787    | Some (uri, metasenv, bo, ty) ->
 788       let currentproof =
 789        (*CSC: Wrong: [] is just plainly wrong *)
 790        Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
 791       in
 792        let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
 793         Cic2acic.acic_object_of_cic_object currentproof
 794        in
 795         let xml, bodyxml =
 796          match
 797           Cic2Xml.print_object uri ~ids_to_inner_sorts
 798            ~ask_dtd_to_the_getter:true acurrentproof
 799          with
 800             xml,Some bodyxml -> xml,bodyxml
 801           | _,None -> assert false
 802         in
 803          Xml.pp ~quiet:true xml (Some prooffiletype) ;
 804          output_html outputhtml
 805           ("<h1 color=\"Green\">Current proof type saved to " ^
 806            prooffiletype ^ "</h1>") ;
 807          Xml.pp ~quiet:true bodyxml (Some prooffile) ;
 808          output_html outputhtml
 809           ("<h1 color=\"Green\">Current proof body saved to " ^
 810            prooffile ^ "</h1>")
 811 ;;
 812
 813 (* Used to typecheck the loaded proofs *)
 814 let typecheck_loaded_proof metasenv bo ty =
 815  let module T = CicTypeChecker in
 816   ignore (
 817    List.fold_left
 818     (fun metasenv ((_,context,ty) as conj) ->
 819       ignore (T.type_of_aux' metasenv context ty) ;
 820       metasenv @ [conj]
 821     ) [] metasenv) ;
 822   ignore (T.type_of_aux' metasenv [] ty) ;
 823   ignore (T.type_of_aux' metasenv [] bo)
 824 ;;
 825
 826 let load () =
 827  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
 828  let output = ((rendering_window ())#output : GMathView.math_view) in
 829  let notebook = (rendering_window ())#notebook in
 830   try
 831    match
 832     GToolbox.input_string ~title:"Load Unfinished Proof" ~text:"/dummy.con"
 833      "Choose an URI:"
 834    with
 835       None -> raise NoChoice
 836     | Some uri0 ->
 837        let uri = UriManager.uri_of_string ("cic:" ^ uri0) in
 838         match CicParser.obj_of_xml prooffiletype (Some prooffile) with
 839            Cic.CurrentProof (_,metasenv,bo,ty,_) ->
 840             typecheck_loaded_proof metasenv bo ty ;
 841             ProofEngine.proof :=
 842              Some (uri, metasenv, bo, ty) ;
 843             ProofEngine.goal :=
 844              (match metasenv with
 845                  [] -> None
 846                | (metano,_,_)::_ -> Some metano
 847              ) ;
 848             refresh_proof output ;
 849             refresh_sequent notebook ;
 850              output_html outputhtml
 851               ("<h1 color=\"Green\">Current proof type loaded from " ^
 852                 prooffiletype ^ "</h1>") ;
 853              output_html outputhtml
 854               ("<h1 color=\"Green\">Current proof body loaded from " ^
 855                 prooffile ^ "</h1>") ;
 856             !save_set_sensitive true
 857          | _ -> assert false
 858   with
 859      RefreshSequentException e ->
 860       output_html outputhtml
 861        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 862         "sequent: " ^ Printexc.to_string e ^ "</h1>")
 863    | RefreshProofException e ->
 864       output_html outputhtml
 865        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 866         "proof: " ^ Printexc.to_string e ^ "</h1>")
 867    | e ->
 868       output_html outputhtml
 869        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 870 ;;
 871
 872 let edit_aliases () =
 873  let chosen = ref false in
 874  let window =
 875   GWindow.window
 876    ~width:400 ~modal:true ~title:"Edit Aliases..." ~border_width:2 () in
 877  let vbox =
 878   GPack.vbox ~border_width:0 ~packing:window#add () in
 879  let scrolled_window =
 880   GBin.scrolled_window ~border_width:10
 881    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
 882  let input = GEdit.text ~editable:true ~width:400 ~height:100
 883    ~packing:scrolled_window#add () in
 884  let hbox =
 885   GPack.hbox ~border_width:0
 886    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 887  let okb =
 888   GButton.button ~label:"Ok"
 889    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 890  let cancelb =
 891   GButton.button ~label:"Cancel"
 892    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 893  ignore (window#connect#destroy GMain.Main.quit) ;
 894  ignore (cancelb#connect#clicked window#destroy) ;
 895  ignore
 896   (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
 897  let dom,resolve_id = !id_to_uris in
 898   ignore
 899    (input#insert_text ~pos:0
 900     (String.concat "\n"
 901       (List.map
 902         (function v ->
 903           let uri =
 904            match resolve_id v with
 905               None -> assert false
 906             | Some uri -> uri
 907           in
 908            "alias " ^ v ^ " " ^
 909              (string_of_cic_textual_parser_uri uri)
 910         ) dom))) ;
 911   window#show () ;
 912   GMain.Main.main () ;
 913   if !chosen then
 914    let dom,resolve_id =
 915     let inputtext = input#get_chars 0 input#length in
 916     let regexpr =
 917      let alfa = "[a-zA-Z_-]" in
 918      let digit = "[0-9]" in
 919      let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in
 920      let blanks = "\( \|\t\|\n\)+" in
 921      let nonblanks = "[^ \t\n]+" in
 922      let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *)
 923       Str.regexp
 924        ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)")
 925     in
 926      let rec aux n =
 927       try
 928        let n' = Str.search_forward regexpr inputtext n in
 929         let id = Str.matched_group 2 inputtext in
 930         let uri =
 931          cic_textual_parser_uri_of_string
 932           ("cic:" ^ (Str.matched_group 5 inputtext))
 933         in
 934          let dom,resolve_id = aux (n' + 1) in
 935           if List.mem id dom then
 936            dom,resolve_id
 937           else
 938            id::dom,
 939             (function id' -> if id = id' then Some uri else resolve_id id')
 940       with
 941        Not_found -> empty_id_to_uris
 942      in
 943       aux 0
 944    in
 945     id_to_uris := dom,resolve_id
 946 ;;
 947
 948 let proveit () =
 949  let module L = LogicalOperations in
 950  let module G = Gdome in
 951  let notebook = (rendering_window ())#notebook in
 952  let output = (rendering_window ())#output in
 953  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
 954   match (rendering_window ())#output#get_selection with
 955     Some node ->
 956      let xpath =
 957       ((node : Gdome.element)#getAttributeNS
 958       (*CSC: OCAML DIVERGE
 959       ((element : G.element)#getAttributeNS
 960       *)
 961         ~namespaceURI:helmns
 962         ~localName:(G.domString "xref"))#to_string
 963      in
 964       if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 965       else
 966        begin
 967         try
 968          match !current_cic_infos with
 969             Some (ids_to_terms, ids_to_father_ids, _, _) ->
 970              let id = xpath in
 971               L.to_sequent id ids_to_terms ids_to_father_ids ;
 972               refresh_proof output ;
 973               refresh_sequent notebook
 974           | None -> assert false (* "ERROR: No current term!!!" *)
 975         with
 976            RefreshSequentException e ->
 977             output_html outputhtml
 978              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 979               "sequent: " ^ Printexc.to_string e ^ "</h1>")
 980          | RefreshProofException e ->
 981             output_html outputhtml
 982              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 983               "proof: " ^ Printexc.to_string e ^ "</h1>")
 984          | e ->
 985             output_html outputhtml
 986              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 987        end
 988   | None -> assert false (* "ERROR: No selection!!!" *)
 989 ;;
 990
 991 let focus () =
 992  let module L = LogicalOperations in
 993  let module G = Gdome in
 994  let notebook = (rendering_window ())#notebook in
 995  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
 996   match (rendering_window ())#output#get_selection with
 997     Some node ->
 998      let xpath =
 999       ((node : Gdome.element)#getAttributeNS
1000       (*CSC: OCAML DIVERGE
1001       ((element : G.element)#getAttributeNS
1002       *)
1003         ~namespaceURI:helmns
1004         ~localName:(G.domString "xref"))#to_string
1005      in
1006       if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1007       else
1008        begin
1009         try
1010          match !current_cic_infos with
1011             Some (ids_to_terms, ids_to_father_ids, _, _) ->
1012              let id = xpath in
1013               L.focus id ids_to_terms ids_to_father_ids ;
1014               refresh_sequent notebook
1015           | None -> assert false (* "ERROR: No current term!!!" *)
1016         with
1017            RefreshSequentException e ->
1018             output_html outputhtml
1019              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1020               "sequent: " ^ Printexc.to_string e ^ "</h1>")
1021          | RefreshProofException e ->
1022             output_html outputhtml
1023              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1024               "proof: " ^ Printexc.to_string e ^ "</h1>")
1025          | e ->
1026             output_html outputhtml
1027              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1028        end
1029   | None -> assert false (* "ERROR: No selection!!!" *)
1030 ;;
1031
1032 exception NoPrevGoal;;
1033 exception NoNextGoal;;
1034
1035 let setgoal metano =
1036  let module L = LogicalOperations in
1037  let module G = Gdome in
1038  let notebook = (rendering_window ())#notebook in
1039  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1040   let metasenv =
1041    match !ProofEngine.proof with
1042       None -> assert false
1043     | Some (_,metasenv,_,_) -> metasenv
1044   in
1045    try
1046     refresh_sequent ~empty_notebook:false notebook
1047    with
1048       RefreshSequentException e ->
1049        output_html outputhtml
1050         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1051          "sequent: " ^ Printexc.to_string e ^ "</h1>")
1052     | e ->
1053        output_html outputhtml
1054         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1055 ;;
1056
1057 let show_in_show_window, show_in_show_window_callback =
1058  let window =
1059   GWindow.window ~width:800 ~border_width:2 () in
1060  let scrolled_window =
1061   GBin.scrolled_window ~border_width:10 ~packing:window#add () in
1062  let mmlwidget =
1063   GMathView.math_view ~packing:scrolled_window#add ~width:600 ~height:400 () in
1064  let _ = window#event#connect#delete (fun _ -> window#misc#hide () ; true ) in
1065  let href = Gdome.domString "href" in
1066   let show_in_show_window uri =
1067    let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1068     try
1069      CicTypeChecker.typecheck uri ;
1070      let obj = CicEnvironment.get_cooked_obj uri in
1071       let
1072        (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
1073         ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
1074       =
1075        Cic2acic.acic_object_of_cic_object obj
1076       in
1077        let mml =
1078         mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts
1079          ids_to_inner_types
1080        in
1081         window#set_title (UriManager.string_of_uri uri) ;
1082         window#misc#hide () ; window#show () ;
1083         mmlwidget#load_tree mml ;
1084     with
1085      e ->
1086       output_html outputhtml
1087        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1088   in
1089    let show_in_show_window_callback mmlwidget (n : Gdome.element) =
1090     if n#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then
1091      let uri =
1092       (n#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string
1093      in
1094       show_in_show_window (UriManager.uri_of_string uri)
1095     else
1096      if mmlwidget#get_action <> None then
1097       mmlwidget#action_toggle
1098    in
1099     let _ =
1100      mmlwidget#connect#clicked (show_in_show_window_callback mmlwidget)
1101     in
1102      show_in_show_window, show_in_show_window_callback
1103 ;;
1104
1105 exception NoObjectsLocated;;
1106
1107 let user_uri_choice ~title ~msg uris =
1108  let uri =
1109   match uris with
1110      [] -> raise NoObjectsLocated
1111    | [uri] -> uri
1112    | uris ->
1113       match
1114        interactive_user_uri_choice ~selection_mode:`SINGLE ~title ~msg uris
1115       with
1116          [uri] -> uri
1117        | _ -> assert false
1118  in
1119   String.sub uri 4 (String.length uri - 4)
1120 ;;
1121
1122 let locate_callback id =
1123  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1124  let result = MQueryGenerator.locate id in
1125  let uris =
1126   List.map
1127    (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
1128    result in
1129  let html =
1130   (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>")
1131  in
1132   output_html outputhtml html ;
1133   user_uri_choice ~title:"Ambiguous input."
1134    ~msg:
1135      ("Ambiguous input \"" ^ id ^
1136       "\". Please, choose one interpetation:")
1137    uris
1138 ;;
1139
1140 let locate () =
1141  let inputt = ((rendering_window ())#inputt : term_editor) in
1142  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1143    try
1144     match
1145      GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:"
1146     with
1147        None -> raise NoChoice
1148      | Some input ->
1149         let uri = locate_callback input in
1150          inputt#set_term uri
1151    with
1152     e ->
1153      output_html outputhtml
1154       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1155 ;;
1156
1157 let input_or_locate_uri ~title =
1158  let uri = ref None in
1159  let window =
1160   GWindow.window
1161    ~width:400 ~modal:true ~title ~border_width:2 () in
1162  let vbox = GPack.vbox ~packing:window#add () in
1163  let hbox1 =
1164   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1165  let _ =
1166   GMisc.label ~text:"Enter a valid URI:" ~packing:(hbox1#pack ~padding:5) () in
1167  let manual_input =
1168   GEdit.entry ~editable:true
1169    ~packing:(hbox1#pack ~expand:true ~fill:true ~padding:5) () in
1170  let checkb =
1171   GButton.button ~label:"Check"
1172    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1173  let _ = checkb#misc#set_sensitive false in
1174  let hbox2 =
1175   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1176  let _ =
1177   GMisc.label ~text:"You can also enter an indentifier to locate:"
1178    ~packing:(hbox2#pack ~padding:5) () in
1179  let locate_input =
1180   GEdit.entry ~editable:true
1181    ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
1182  let locateb =
1183   GButton.button ~label:"Locate"
1184    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1185  let _ = locateb#misc#set_sensitive false in
1186  let hbox3 =
1187   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1188  let okb =
1189   GButton.button ~label:"Ok"
1190    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1191  let _ = okb#misc#set_sensitive false in
1192  let cancelb =
1193   GButton.button ~label:"Cancel"
1194    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) ()
1195  in
1196   ignore (window#connect#destroy GMain.Main.quit) ;
1197   ignore
1198    (cancelb#connect#clicked (function () -> uri := None ; window#destroy ())) ;
1199   let check_callback () =
1200    let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1201    let uri = "cic:" ^ manual_input#text in
1202     try
1203       ignore (Getter.resolve (UriManager.uri_of_string uri)) ;
1204       output_html outputhtml "<h1 color=\"Green\">OK</h1>" ;
1205       true
1206     with
1207        Getter.Unresolved ->
1208         output_html outputhtml
1209          ("<h1 color=\"Red\">URI " ^ uri ^
1210           " does not correspond to any object.</h1>") ;
1211         false
1212      | UriManager.IllFormedUri _ ->
1213         output_html outputhtml
1214          ("<h1 color=\"Red\">URI " ^ uri ^ " is not well-formed.</h1>") ;
1215         false
1216      | e ->
1217         output_html outputhtml
1218          ("<h1 color=\"Red\">" ^ Printexc.to_string e ^ "</h1>") ;
1219         false
1220   in
1221   ignore
1222    (okb#connect#clicked
1223      (function () ->
1224        if check_callback () then
1225         begin
1226          uri := Some manual_input#text ;
1227          window#destroy ()
1228         end
1229    )) ;
1230   ignore (checkb#connect#clicked (function () -> ignore (check_callback ()))) ;
1231   ignore
1232    (manual_input#connect#changed
1233      (fun _ ->
1234        if manual_input#text = "" then
1235         begin
1236          checkb#misc#set_sensitive false ;
1237          okb#misc#set_sensitive false
1238         end
1239        else
1240         begin
1241          checkb#misc#set_sensitive true ;
1242          okb#misc#set_sensitive true
1243         end));
1244   ignore
1245    (locate_input#connect#changed
1246      (fun _ -> locateb#misc#set_sensitive (locate_input#text <> ""))) ;
1247   ignore
1248    (locateb#connect#clicked
1249      (function () ->
1250        let id = locate_input#text in
1251         manual_input#set_text (locate_callback id) ;
1252         locate_input#delete_text 0 (String.length id)
1253    )) ;
1254   window#show () ;
1255   GMain.Main.main () ;
1256   match !uri with
1257      None -> raise NoChoice
1258    | Some uri -> UriManager.uri_of_string ("cic:" ^ uri)
1259 ;;
1260
1261 let locate_one_id id =
1262  let result = MQueryGenerator.locate id in
1263  let uris =
1264   List.map
1265    (function uri,_ ->
1266      wrong_xpointer_format_from_wrong_xpointer_format' uri
1267    ) result in
1268  let html= " <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>" in
1269   output_html (rendering_window ())#outputhtml html ;
1270   let uris' =
1271    match uris with
1272       [] ->
1273        [UriManager.string_of_uri
1274          (input_or_locate_uri ~title:("URI matching \"" ^ id ^ "\" unknown."))]
1275     | [uri] -> [uri]
1276     | _ ->
1277       interactive_user_uri_choice
1278        ~selection_mode:`EXTENDED
1279        ~ok:"Try every selection."
1280        ~title:"Ambiguous input."
1281        ~msg:
1282          ("Ambiguous input \"" ^ id ^
1283           "\". Please, choose one or more interpretations:")
1284        uris
1285   in
1286    List.map cic_textual_parser_uri_of_string uris'
1287 ;;
1288
1289 exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput;;
1290 exception AmbiguousInput;;
1291
1292 let disambiguate_input context metasenv dom mk_metasenv_and_expr =
1293  let known_ids,resolve_id = !id_to_uris in
1294  let dom' =
1295   let rec filter =
1296    function
1297       [] -> []
1298     | he::tl ->
1299        if List.mem he known_ids then filter tl else he::(filter tl)
1300   in
1301    filter dom
1302  in
1303   (* for each id in dom' we get the list of uris associated to it *)
1304   let list_of_uris = List.map locate_one_id dom' in
1305   (* and now we compute the list of all possible assignments from id to uris *)
1306   let resolve_ids =
1307    let rec aux ids list_of_uris =
1308     match ids,list_of_uris with
1309        [],[] -> [resolve_id]
1310      | id::idtl,uris::uristl ->
1311         let resolves = aux idtl uristl in
1312          List.concat
1313           (List.map
1314             (function uri ->
1315               List.map
1316                (function f ->
1317                  function id' -> if id = id' then Some uri else f id'
1318                ) resolves
1319             ) uris
1320           )
1321      | _,_ -> assert false
1322    in
1323     aux dom' list_of_uris
1324   in
1325    let tests_no = List.length resolve_ids in
1326     if tests_no > 1 then
1327      output_html (outputhtml ())
1328       ("<h1>Disambiguation phase started: " ^
1329         string_of_int (List.length resolve_ids) ^ " cases will be tried.") ;
1330    (* now we select only the ones that generates well-typed terms *)
1331    let resolve_ids' =
1332     let rec filter =
1333      function
1334         [] -> []
1335       | resolve::tl ->
1336          let metasenv',expr = mk_metasenv_and_expr resolve in
1337           try
1338 (*CSC: Bug here: we do not try to typecheck also the metasenv' *)
1339            ignore
1340             (CicTypeChecker.type_of_aux' metasenv context expr) ;
1341            resolve::(filter tl)
1342           with
1343            _ -> filter tl
1344     in
1345      filter resolve_ids
1346    in
1347     let resolve_id' =
1348      match resolve_ids' with
1349         [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
1350       | [resolve_id] -> resolve_id
1351       | _ ->
1352         let choices =
1353          List.map
1354           (function resolve ->
1355             List.map
1356              (function id ->
1357                id,
1358                 match resolve id with
1359                    None -> assert false
1360                  | Some uri ->
1361                     match uri with
1362                        CicTextualParser0.ConUri uri
1363                      | CicTextualParser0.VarUri uri ->
1364                         UriManager.string_of_uri uri
1365                      | CicTextualParser0.IndTyUri (uri,tyno) ->
1366                         UriManager.string_of_uri uri ^ "#xpointer(1/" ^
1367                          string_of_int (tyno+1) ^ ")"
1368                      | CicTextualParser0.IndConUri (uri,tyno,consno) ->
1369                         UriManager.string_of_uri uri ^ "#xpointer(1/" ^
1370                          string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^                           ")"
1371              ) dom
1372           ) resolve_ids'
1373         in
1374          let index = interactive_interpretation_choice choices in
1375           List.nth resolve_ids' index
1376     in
1377      id_to_uris := known_ids @ dom', resolve_id' ;
1378      mk_metasenv_and_expr resolve_id'
1379 ;;
1380
1381 exception UriAlreadyInUse;;
1382 exception NotAUriToAConstant;;
1383
1384 let new_proof () =
1385  let inputt = ((rendering_window ())#inputt : term_editor) in
1386  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1387  let output = ((rendering_window ())#output : GMathView.math_view) in
1388  let notebook = (rendering_window ())#notebook in
1389
1390  let chosen = ref false in
1391  let get_parsed = ref (function _ -> assert false) in
1392  let get_uri = ref (function _ -> assert false) in
1393  let non_empty_type = ref false in
1394  let window =
1395   GWindow.window
1396    ~width:600 ~modal:true ~title:"New Proof or Definition"
1397    ~border_width:2 () in
1398  let vbox = GPack.vbox ~packing:window#add () in
1399  let hbox =
1400   GPack.hbox ~border_width:0
1401    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1402  let _ =
1403   GMisc.label ~text:"Enter the URI for the new theorem or definition:"
1404    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1405  let uri_entry =
1406   GEdit.entry ~editable:true
1407    ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1408  let hbox1 =
1409   GPack.hbox ~border_width:0
1410    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1411  let _ =
1412   GMisc.label ~text:"Enter the theorem or definition type:"
1413    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1414  let scrolled_window =
1415   GBin.scrolled_window ~border_width:5
1416    ~packing:(vbox#pack ~expand:true ~padding:0) () in
1417  (* the content of the scrolled_window is moved below (see comment) *)
1418  let hbox =
1419   GPack.hbox ~border_width:0
1420    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1421  let okb =
1422   GButton.button ~label:"Ok"
1423    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1424  let _ = okb#misc#set_sensitive false in
1425  let cancelb =
1426   GButton.button ~label:"Cancel"
1427    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1428  (* moved here to have visibility of the ok button *)
1429  let newinputt =
1430   new term_editor ~width:400 ~height:100 ~packing:scrolled_window#add ()
1431    ~isnotempty_callback:
1432     (function b ->
1433       non_empty_type := b ;
1434       okb#misc#set_sensitive (b && uri_entry#text <> ""))
1435  in
1436  let _ =
1437   newinputt#set_term inputt#get_as_string ;
1438   inputt#reset in
1439  let _ =
1440   uri_entry#connect#changed
1441    (function () ->
1442      okb#misc#set_sensitive (!non_empty_type && uri_entry#text <> ""))
1443  in
1444  ignore (window#connect#destroy GMain.Main.quit) ;
1445  ignore (cancelb#connect#clicked window#destroy) ;
1446  ignore
1447   (okb#connect#clicked
1448     (function () ->
1449       chosen := true ;
1450       try
1451        let parsed = newinputt#get_term [] [] in
1452        let uristr = "cic:" ^ uri_entry#text in
1453        let uri = UriManager.uri_of_string uristr in
1454         if String.sub uristr (String.length uristr - 4) 4 <> ".con" then
1455          raise NotAUriToAConstant
1456         else
1457          begin
1458           try
1459            ignore (Getter.resolve uri) ;
1460            raise UriAlreadyInUse
1461           with
1462            Getter.Unresolved ->
1463             get_parsed := (function () -> parsed) ;
1464             get_uri := (function () -> uri) ;
1465             window#destroy ()
1466          end
1467       with
1468        e ->
1469         output_html outputhtml
1470          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1471   )) ;
1472  window#show () ;
1473  GMain.Main.main () ;
1474  if !chosen then
1475   try
1476    let dom,mk_metasenv_and_expr = !get_parsed () in
1477     let metasenv,expr =
1478      disambiguate_input [] [] dom mk_metasenv_and_expr
1479     in
1480      let _  = CicTypeChecker.type_of_aux' metasenv [] expr in
1481       ProofEngine.proof :=
1482        Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
1483       ProofEngine.goal := Some 1 ;
1484       refresh_sequent notebook ;
1485       refresh_proof output ;
1486       !save_set_sensitive true ;
1487       inputt#reset
1488   with
1489      RefreshSequentException e ->
1490       output_html outputhtml
1491        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1492         "sequent: " ^ Printexc.to_string e ^ "</h1>")
1493    | RefreshProofException e ->
1494       output_html outputhtml
1495        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1496         "proof: " ^ Printexc.to_string e ^ "</h1>")
1497    | e ->
1498       output_html outputhtml
1499        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1500 ;;
1501
1502 let check_term_in_scratch scratch_window metasenv context expr =
1503  try
1504   let ty  = CicTypeChecker.type_of_aux' metasenv context expr in
1505    let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
1506 prerr_endline ("### " ^ CicPp.ppterm expr ^ " ==> " ^ CicPp.ppterm ty) ;
1507     scratch_window#show () ;
1508     scratch_window#mmlwidget#load_tree ~dom:mml
1509  with
1510   e ->
1511    print_endline ("? " ^ CicPp.ppterm expr) ;
1512    raise e
1513 ;;
1514
1515 let check scratch_window () =
1516  let inputt = ((rendering_window ())#inputt : term_editor) in
1517  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1518   let metasenv =
1519    match !ProofEngine.proof with
1520       None -> []
1521     | Some (_,metasenv,_,_) -> metasenv
1522   in
1523   let context,names_context =
1524    let context =
1525     match !ProofEngine.goal with
1526        None -> []
1527      | Some metano ->
1528         let (_,canonical_context,_) =
1529          List.find (function (m,_,_) -> m=metano) metasenv
1530         in
1531          canonical_context
1532    in
1533     context,
1534     List.map
1535      (function
1536          Some (n,_) -> Some n
1537        | None -> None
1538      ) context
1539   in
1540    try
1541     let dom,mk_metasenv_and_expr = inputt#get_term names_context metasenv in
1542      let (metasenv',expr) =
1543       disambiguate_input context metasenv dom mk_metasenv_and_expr
1544      in
1545       check_term_in_scratch scratch_window metasenv' context expr
1546    with
1547     e ->
1548      output_html outputhtml
1549       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1550 ;;
1551
1552
1553 (***********************)
1554 (*       TACTICS       *)
1555 (***********************)
1556
1557 let call_tactic tactic () =
1558  let notebook = (rendering_window ())#notebook in
1559  let output = ((rendering_window ())#output : GMathView.math_view) in
1560  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1561  let savedproof = !ProofEngine.proof in
1562  let savedgoal  = !ProofEngine.goal in
1563   begin
1564    try
1565     tactic () ;
1566     refresh_sequent notebook ;
1567     refresh_proof output
1568    with
1569       RefreshSequentException e ->
1570        output_html outputhtml
1571         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1572          "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1573        ProofEngine.proof := savedproof ;
1574        ProofEngine.goal := savedgoal ;
1575        refresh_sequent notebook
1576     | RefreshProofException e ->
1577        output_html outputhtml
1578         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1579          "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1580        ProofEngine.proof := savedproof ;
1581        ProofEngine.goal := savedgoal ;
1582        refresh_sequent notebook ;
1583        refresh_proof output
1584     | e ->
1585        output_html outputhtml
1586         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1587        ProofEngine.proof := savedproof ;
1588        ProofEngine.goal := savedgoal ;
1589   end
1590 ;;
1591
1592 let call_tactic_with_input tactic () =
1593  let notebook = (rendering_window ())#notebook in
1594  let output = ((rendering_window ())#output : GMathView.math_view) in
1595  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1596  let inputt = ((rendering_window ())#inputt : term_editor) in
1597  let savedproof = !ProofEngine.proof in
1598  let savedgoal  = !ProofEngine.goal in
1599   let uri,metasenv,bo,ty =
1600    match !ProofEngine.proof with
1601       None -> assert false
1602     | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
1603   in
1604    let canonical_context =
1605     match !ProofEngine.goal with
1606        None -> assert false
1607      | Some metano ->
1608         let (_,canonical_context,_) =
1609          List.find (function (m,_,_) -> m=metano) metasenv
1610         in
1611          canonical_context
1612    in
1613    let context =
1614     List.map
1615      (function
1616          Some (n,_) -> Some n
1617        | None -> None
1618      ) canonical_context
1619    in
1620     try
1621      let dom,mk_metasenv_and_expr = inputt#get_term context metasenv in
1622       let (metasenv',expr) =
1623        disambiguate_input canonical_context metasenv dom mk_metasenv_and_expr
1624       in
1625        ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
1626        tactic expr ;
1627        refresh_sequent notebook ;
1628        refresh_proof output ;
1629        inputt#reset
1630     with
1631        RefreshSequentException e ->
1632         output_html outputhtml
1633          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1634           "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1635         ProofEngine.proof := savedproof ;
1636         ProofEngine.goal := savedgoal ;
1637         refresh_sequent notebook
1638      | RefreshProofException e ->
1639         output_html outputhtml
1640          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1641           "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1642         ProofEngine.proof := savedproof ;
1643         ProofEngine.goal := savedgoal ;
1644         refresh_sequent notebook ;
1645         refresh_proof output
1646      | e ->
1647         output_html outputhtml
1648          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1649         ProofEngine.proof := savedproof ;
1650         ProofEngine.goal := savedgoal ;
1651 ;;
1652
1653 let call_tactic_with_goal_input tactic () =
1654  let module L = LogicalOperations in
1655  let module G = Gdome in
1656   let notebook = (rendering_window ())#notebook in
1657   let output = ((rendering_window ())#output : GMathView.math_view) in
1658   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1659   let savedproof = !ProofEngine.proof in
1660   let savedgoal  = !ProofEngine.goal in
1661    match notebook#proofw#get_selection with
1662      Some node ->
1663       let xpath =
1664        ((node : Gdome.element)#getAttributeNS
1665          ~namespaceURI:helmns
1666          ~localName:(G.domString "xref"))#to_string
1667       in
1668        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1669        else
1670         begin
1671          try
1672           match !current_goal_infos with
1673              Some (ids_to_terms, ids_to_father_ids,_) ->
1674               let id = xpath in
1675                tactic (Hashtbl.find ids_to_terms id) ;
1676                refresh_sequent notebook ;
1677                refresh_proof output
1678            | None -> assert false (* "ERROR: No current term!!!" *)
1679          with
1680             RefreshSequentException e ->
1681              output_html outputhtml
1682               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1683                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1684              ProofEngine.proof := savedproof ;
1685              ProofEngine.goal := savedgoal ;
1686              refresh_sequent notebook
1687           | RefreshProofException e ->
1688              output_html outputhtml
1689               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1690                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1691              ProofEngine.proof := savedproof ;
1692              ProofEngine.goal := savedgoal ;
1693              refresh_sequent notebook ;
1694              refresh_proof output
1695           | e ->
1696              output_html outputhtml
1697               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1698              ProofEngine.proof := savedproof ;
1699              ProofEngine.goal := savedgoal ;
1700         end
1701    | None ->
1702       output_html outputhtml
1703        ("<h1 color=\"red\">No term selected</h1>")
1704 ;;
1705
1706 let call_tactic_with_input_and_goal_input tactic () =
1707  let module L = LogicalOperations in
1708  let module G = Gdome in
1709   let notebook = (rendering_window ())#notebook in
1710   let output = ((rendering_window ())#output : GMathView.math_view) in
1711   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1712   let inputt = ((rendering_window ())#inputt : term_editor) in
1713   let savedproof = !ProofEngine.proof in
1714   let savedgoal  = !ProofEngine.goal in
1715    match notebook#proofw#get_selection with
1716      Some node ->
1717       let xpath =
1718        ((node : Gdome.element)#getAttributeNS
1719          ~namespaceURI:helmns
1720          ~localName:(G.domString "xref"))#to_string
1721       in
1722        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1723        else
1724         begin
1725          try
1726           match !current_goal_infos with
1727              Some (ids_to_terms, ids_to_father_ids,_) ->
1728               let id = xpath in
1729                let uri,metasenv,bo,ty =
1730                 match !ProofEngine.proof with
1731                    None -> assert false
1732                  | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
1733                in
1734                 let canonical_context =
1735                  match !ProofEngine.goal with
1736                     None -> assert false
1737                   | Some metano ->
1738                      let (_,canonical_context,_) =
1739                       List.find (function (m,_,_) -> m=metano) metasenv
1740                      in
1741                       canonical_context in
1742                 let context =
1743                  List.map
1744                   (function
1745                       Some (n,_) -> Some n
1746                     | None -> None
1747                   ) canonical_context
1748                 in
1749                  let dom,mk_metasenv_and_expr = inputt#get_term context metasenv
1750                  in
1751                   let (metasenv',expr) =
1752                    disambiguate_input canonical_context metasenv dom
1753                     mk_metasenv_and_expr
1754                   in
1755                    ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
1756                    tactic ~goal_input:(Hashtbl.find ids_to_terms id)
1757                     ~input:expr ;
1758                    refresh_sequent notebook ;
1759                    refresh_proof output ;
1760                    inputt#reset
1761            | None -> assert false (* "ERROR: No current term!!!" *)
1762          with
1763             RefreshSequentException e ->
1764              output_html outputhtml
1765               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1766                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1767              ProofEngine.proof := savedproof ;
1768              ProofEngine.goal := savedgoal ;
1769              refresh_sequent notebook
1770           | RefreshProofException e ->
1771              output_html outputhtml
1772               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1773                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1774              ProofEngine.proof := savedproof ;
1775              ProofEngine.goal := savedgoal ;
1776              refresh_sequent notebook ;
1777              refresh_proof output
1778           | e ->
1779              output_html outputhtml
1780               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1781              ProofEngine.proof := savedproof ;
1782              ProofEngine.goal := savedgoal ;
1783         end
1784    | None ->
1785       output_html outputhtml
1786        ("<h1 color=\"red\">No term selected</h1>")
1787 ;;
1788
1789 let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
1790  let module L = LogicalOperations in
1791  let module G = Gdome in
1792   let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in
1793   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1794   let savedproof = !ProofEngine.proof in
1795   let savedgoal  = !ProofEngine.goal in
1796    match mmlwidget#get_selection with
1797      Some node ->
1798       let xpath =
1799        ((node : Gdome.element)#getAttributeNS
1800          ~namespaceURI:helmns
1801          ~localName:(G.domString "xref"))#to_string
1802       in
1803        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1804        else
1805         begin
1806          try
1807           match !current_scratch_infos with
1808              (* term is the whole goal in the scratch_area *)
1809              Some (term,ids_to_terms, ids_to_father_ids,_) ->
1810               let id = xpath in
1811                let expr = tactic term (Hashtbl.find ids_to_terms id) in
1812                 let mml = mml_of_cic_term 111 expr in
1813                  scratch_window#show () ;
1814                  scratch_window#mmlwidget#load_tree ~dom:mml
1815            | None -> assert false (* "ERROR: No current term!!!" *)
1816          with
1817           e ->
1818            output_html outputhtml
1819             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1820         end
1821    | None ->
1822       output_html outputhtml
1823        ("<h1 color=\"red\">No term selected</h1>")
1824 ;;
1825
1826 let call_tactic_with_hypothesis_input tactic () =
1827  let module L = LogicalOperations in
1828  let module G = Gdome in
1829   let notebook = (rendering_window ())#notebook in
1830   let output = ((rendering_window ())#output : GMathView.math_view) in
1831   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1832   let savedproof = !ProofEngine.proof in
1833   let savedgoal  = !ProofEngine.goal in
1834    match notebook#proofw#get_selection with
1835      Some node ->
1836       let xpath =
1837        ((node : Gdome.element)#getAttributeNS
1838          ~namespaceURI:helmns
1839          ~localName:(G.domString "xref"))#to_string
1840       in
1841        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1842        else
1843         begin
1844          try
1845           match !current_goal_infos with
1846              Some (_,_,ids_to_hypotheses) ->
1847               let id = xpath in
1848                tactic (Hashtbl.find ids_to_hypotheses id) ;
1849                refresh_sequent notebook ;
1850                refresh_proof output
1851            | None -> assert false (* "ERROR: No current term!!!" *)
1852          with
1853             RefreshSequentException e ->
1854              output_html outputhtml
1855               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1856                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1857              ProofEngine.proof := savedproof ;
1858              ProofEngine.goal := savedgoal ;
1859              refresh_sequent notebook
1860           | RefreshProofException e ->
1861              output_html outputhtml
1862               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1863                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1864              ProofEngine.proof := savedproof ;
1865              ProofEngine.goal := savedgoal ;
1866              refresh_sequent notebook ;
1867              refresh_proof output
1868           | e ->
1869              output_html outputhtml
1870               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1871              ProofEngine.proof := savedproof ;
1872              ProofEngine.goal := savedgoal ;
1873         end
1874    | None ->
1875       output_html outputhtml
1876        ("<h1 color=\"red\">No term selected</h1>")
1877 ;;
1878
1879
1880 let intros = call_tactic ProofEngine.intros;;
1881 let exact = call_tactic_with_input ProofEngine.exact;;
1882 let apply = call_tactic_with_input ProofEngine.apply;;
1883 let elimsimplintros = call_tactic_with_input ProofEngine.elim_simpl_intros;;
1884 let elimtype = call_tactic_with_input ProofEngine.elim_type;;
1885 let whd = call_tactic_with_goal_input ProofEngine.whd;;
1886 let reduce = call_tactic_with_goal_input ProofEngine.reduce;;
1887 let simpl = call_tactic_with_goal_input ProofEngine.simpl;;
1888 let fold = call_tactic_with_input ProofEngine.fold;;
1889 let cut = call_tactic_with_input ProofEngine.cut;;
1890 let change = call_tactic_with_input_and_goal_input ProofEngine.change;;
1891 let letin = call_tactic_with_input ProofEngine.letin;;
1892 let ring = call_tactic ProofEngine.ring;;
1893 let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody;;
1894 let clear = call_tactic_with_hypothesis_input ProofEngine.clear;;
1895 let fourier = call_tactic ProofEngine.fourier;;
1896 let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl;;
1897 let reflexivity = call_tactic ProofEngine.reflexivity;;
1898 let symmetry = call_tactic ProofEngine.symmetry;;
1899 let transitivity = call_tactic_with_input ProofEngine.transitivity;;
1900 let exists = call_tactic ProofEngine.exists;;
1901 let split = call_tactic ProofEngine.split;;
1902 let left = call_tactic ProofEngine.left;;
1903 let right = call_tactic ProofEngine.right;;
1904 let assumption = call_tactic ProofEngine.assumption;;
1905 let generalize = call_tactic_with_goal_input ProofEngine.generalize;;
1906 let absurd = call_tactic_with_input ProofEngine.absurd;;
1907 let contradiction = call_tactic ProofEngine.contradiction;;
1908 (* Galla: come dare alla tattica la lista di termini da decomporre?
1909 let decompose = call_tactic_with_input_and_goal_input ProofEngine.decompose;;
1910 *)
1911
1912 let whd_in_scratch scratch_window =
1913  call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
1914   scratch_window
1915 ;;
1916 let reduce_in_scratch scratch_window =
1917  call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch
1918   scratch_window
1919 ;;
1920 let simpl_in_scratch scratch_window =
1921  call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch
1922   scratch_window
1923 ;;
1924
1925
1926
1927 (**********************)
1928 (*   END OF TACTICS   *)
1929 (**********************)
1930
1931
1932 let show () =
1933  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1934   try
1935    show_in_show_window (input_or_locate_uri ~title:"Show")
1936   with
1937    e ->
1938     output_html outputhtml
1939      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1940 ;;
1941
1942 exception NotADefinition;;
1943
1944 let open_ () =
1945  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1946  let output = ((rendering_window ())#output : GMathView.math_view) in
1947  let notebook = (rendering_window ())#notebook in
1948    try
1949     let uri = input_or_locate_uri ~title:"Open" in
1950      CicTypeChecker.typecheck uri ;
1951      let metasenv,bo,ty =
1952       match CicEnvironment.get_cooked_obj uri with
1953          Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
1954        | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
1955        | Cic.Constant _
1956        | Cic.Variable _
1957        | Cic.InductiveDefinition _ -> raise NotADefinition
1958      in
1959       ProofEngine.proof :=
1960        Some (uri, metasenv, bo, ty) ;
1961       ProofEngine.goal := None ;
1962       refresh_sequent notebook ;
1963       refresh_proof output
1964    with
1965       RefreshSequentException e ->
1966        output_html outputhtml
1967         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1968          "sequent: " ^ Printexc.to_string e ^ "</h1>")
1969     | RefreshProofException e ->
1970        output_html outputhtml
1971         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1972          "proof: " ^ Printexc.to_string e ^ "</h1>")
1973     | e ->
1974        output_html outputhtml
1975         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1976 ;;
1977
1978
1979 let searchPattern () =
1980  let inputt = ((rendering_window ())#inputt : term_editor) in
1981  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1982   try
1983    let rec get_level ?(last_invalid=false) () =
1984     match
1985      GToolbox.input_string
1986       ~title:"Insert the strictness parameter for the query:"
1987       ((if last_invalid then
1988          "Invalid input (must be a non-negative natural number). Insert again "
1989         else
1990          "Insert "
1991        ) ^ "the strictness parameter for the query:")
1992     with
1993        None -> raise NoChoice
1994      | Some n ->
1995         try
1996          int_of_string n
1997         with
1998          _ -> get_level ~last_invalid:true ()
1999    in
2000     let level = get_level () in
2001     let metasenv =
2002      match !ProofEngine.proof with
2003         None -> assert false
2004       | Some (_,metasenv,_,_) -> metasenv
2005     in
2006      match !ProofEngine.goal with
2007         None -> ()
2008       | Some metano ->
2009          let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
2010           let list_of_must,can = MQueryLevels.out_restr metasenv ey ty in
2011           let len = List.length list_of_must in
2012           let must = if level < len then List.nth list_of_must level else can in
2013           let result = MQueryGenerator.searchPattern metasenv ey ty must can in
2014           let uris =
2015            List.map
2016             (function uri,_ ->
2017               wrong_xpointer_format_from_wrong_xpointer_format' uri
2018             ) result in
2019           let html =
2020            " <h1>Backward Query: </h1>" ^
2021            " <h2>Levels: </h2> " ^
2022            MQueryLevels.string_of_levels
2023             (MQueryLevels.levels_of_term metasenv ey ty) "<br>" ^
2024            " <pre>" ^ get_last_query result ^ "</pre>"
2025           in
2026            output_html outputhtml html ;
2027            let uris',exc =
2028             let rec filter_out =
2029              function
2030                 [] -> [],""
2031               | uri::tl ->
2032                  let tl',exc = filter_out tl in
2033                   try
2034                    if
2035                     ProofEngine.can_apply
2036                      (term_of_cic_textual_parser_uri
2037                       (cic_textual_parser_uri_of_string uri))
2038                    then
2039                     uri::tl',exc
2040                    else
2041                     tl',exc
2042                   with
2043                    e ->
2044                     let exc' =
2045                      "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
2046                       uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
2047                     in
2048                      tl',exc'
2049             in
2050              filter_out uris
2051            in
2052             let html' =
2053              " <h1>Objects that can actually be applied: </h1> " ^
2054              String.concat "<br>" uris' ^ exc ^
2055              " <h1>Number of false matches: " ^
2056               string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
2057              " <h1>Number of good matches: " ^
2058               string_of_int (List.length uris') ^ "</h1>"
2059             in
2060              output_html outputhtml html' ;
2061              let uri' =
2062               user_uri_choice ~title:"Ambiguous input."
2063               ~msg:
2064                 "Many lemmas can be successfully applied. Please, choose one:"
2065                uris'
2066              in
2067               inputt#set_term uri' ;
2068               apply ()
2069   with
2070    e ->
2071     output_html outputhtml
2072      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2073 ;;
2074
2075 let choose_selection
2076      (mmlwidget : GMathView.math_view) (element : Gdome.element option)
2077 =
2078  let module G = Gdome in
2079   let rec aux element =
2080    if element#hasAttributeNS
2081        ~namespaceURI:helmns
2082        ~localName:(G.domString "xref")
2083    then
2084      mmlwidget#set_selection (Some element)
2085    else
2086       match element#get_parentNode with
2087          None -> assert false
2088        (*CSC: OCAML DIVERGES!
2089        | Some p -> aux (new G.element_of_node p)
2090        *)
2091        | Some p -> aux (new Gdome.element_of_node p)
2092   in
2093    match element with
2094      Some x -> aux x
2095    | None   -> mmlwidget#set_selection None
2096 ;;
2097
2098 (* STUFF TO BUILD THE GTK INTERFACE *)
2099
2100 (* Stuff for the widget settings *)
2101
2102 let export_to_postscript (output : GMathView.math_view) =
2103  let lastdir = ref (Unix.getcwd ()) in
2104   function () ->
2105    match
2106     GToolbox.select_file ~title:"Export to PostScript"
2107      ~dir:lastdir ~filename:"screenshot.ps" ()
2108    with
2109       None -> ()
2110     | Some filename ->
2111        output#export_to_postscript ~filename:filename ();
2112 ;;
2113
2114 let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
2115  button_set_kerning button_set_transparency export_to_postscript_menu_item
2116  button_t1 ()
2117 =
2118  let is_set = button_t1#active in
2119   output#set_font_manager_type
2120    (if is_set then `font_manager_t1 else `font_manager_gtk) ;
2121   if is_set then
2122    begin
2123     button_set_anti_aliasing#misc#set_sensitive true ;
2124     button_set_kerning#misc#set_sensitive true ;
2125     button_set_transparency#misc#set_sensitive true ;
2126     export_to_postscript_menu_item#misc#set_sensitive true ;
2127    end
2128   else
2129    begin
2130     button_set_anti_aliasing#misc#set_sensitive false ;
2131     button_set_kerning#misc#set_sensitive false ;
2132     button_set_transparency#misc#set_sensitive false ;
2133     export_to_postscript_menu_item#misc#set_sensitive false ;
2134    end
2135 ;;
2136
2137 let set_anti_aliasing output button_set_anti_aliasing () =
2138  output#set_anti_aliasing button_set_anti_aliasing#active
2139 ;;
2140
2141 let set_kerning output button_set_kerning () =
2142  output#set_kerning button_set_kerning#active
2143 ;;
2144
2145 let set_transparency output button_set_transparency () =
2146  output#set_transparency button_set_transparency#active
2147 ;;
2148
2149 let changefont output font_size_spinb () =
2150  output#set_font_size font_size_spinb#value_as_int
2151 ;;
2152
2153 let set_log_verbosity output log_verbosity_spinb () =
2154  output#set_log_verbosity log_verbosity_spinb#value_as_int
2155 ;;
2156
2157 class settings_window (output : GMathView.math_view) sw
2158  export_to_postscript_menu_item selection_changed_callback
2159 =
2160  let settings_window = GWindow.window ~title:"GtkMathView settings" () in
2161  let vbox =
2162   GPack.vbox ~packing:settings_window#add () in
2163  let table =
2164   GPack.table
2165    ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
2166    ~border_width:5 ~packing:vbox#add () in
2167  let button_t1 =
2168   GButton.toggle_button ~label:"activate t1 fonts"
2169    ~packing:(table#attach ~left:0 ~top:0) () in
2170  let button_set_anti_aliasing =
2171   GButton.toggle_button ~label:"set_anti_aliasing"
2172    ~packing:(table#attach ~left:0 ~top:1) () in
2173  let button_set_kerning =
2174   GButton.toggle_button ~label:"set_kerning"
2175    ~packing:(table#attach ~left:1 ~top:1) () in
2176  let button_set_transparency =
2177   GButton.toggle_button ~label:"set_transparency"
2178    ~packing:(table#attach ~left:2 ~top:1) () in
2179  let table =
2180   GPack.table
2181    ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
2182    ~border_width:5 ~packing:vbox#add () in
2183  let font_size_label =
2184   GMisc.label ~text:"font size:"
2185    ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
2186  let font_size_spinb =
2187   let sadj =
2188    GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
2189   in
2190    GEdit.spin_button
2191     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
2192  let log_verbosity_label =
2193   GMisc.label ~text:"log verbosity:"
2194    ~packing:(table#attach ~left:0 ~top:1) () in
2195  let log_verbosity_spinb =
2196   let sadj =
2197    GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
2198   in
2199    GEdit.spin_button
2200     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
2201  let hbox =
2202   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2203  let closeb =
2204   GButton.button ~label:"Close"
2205    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2206 object(self)
2207  method show = settings_window#show
2208  initializer
2209   button_set_anti_aliasing#misc#set_sensitive false ;
2210   button_set_kerning#misc#set_sensitive false ;
2211   button_set_transparency#misc#set_sensitive false ;
2212   (* Signals connection *)
2213   ignore(button_t1#connect#clicked
2214    (activate_t1 output button_set_anti_aliasing button_set_kerning
2215     button_set_transparency export_to_postscript_menu_item button_t1)) ;
2216   ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
2217   ignore(button_set_anti_aliasing#connect#toggled
2218    (set_anti_aliasing output button_set_anti_aliasing));
2219   ignore(button_set_kerning#connect#toggled
2220    (set_kerning output button_set_kerning)) ;
2221   ignore(button_set_transparency#connect#toggled
2222    (set_transparency output button_set_transparency)) ;
2223   ignore(log_verbosity_spinb#connect#changed
2224    (set_log_verbosity output log_verbosity_spinb)) ;
2225   ignore(closeb#connect#clicked settings_window#misc#hide)
2226 end;;
2227
2228 (* Scratch window *)
2229
2230 class scratch_window =
2231  let window =
2232   GWindow.window ~title:"MathML viewer" ~border_width:2 () in
2233  let vbox =
2234   GPack.vbox ~packing:window#add () in
2235  let hbox =
2236   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2237  let whdb =
2238   GButton.button ~label:"Whd"
2239    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2240  let reduceb =
2241   GButton.button ~label:"Reduce"
2242    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2243  let simplb =
2244   GButton.button ~label:"Simpl"
2245    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2246  let scrolled_window =
2247   GBin.scrolled_window ~border_width:10
2248    ~packing:(vbox#pack ~expand:true ~padding:5) () in
2249  let mmlwidget =
2250   GMathView.math_view
2251    ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
2252 object(self)
2253  method mmlwidget = mmlwidget
2254  method show () = window#misc#hide () ; window#show ()
2255  initializer
2256   ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
2257   ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
2258   ignore(whdb#connect#clicked (whd_in_scratch self)) ;
2259   ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
2260   ignore(simplb#connect#clicked (simpl_in_scratch self))
2261 end;;
2262
2263 class page () =
2264  let vbox1 = GPack.vbox () in
2265 object(self)
2266  val mutable proofw_ref = None
2267  val mutable compute_ref = None
2268  method proofw =
2269   Lazy.force self#compute ;
2270   match proofw_ref with
2271      None -> assert false
2272    | Some proofw -> proofw
2273  method content = vbox1
2274  method compute =
2275   match compute_ref with
2276      None -> assert false
2277    | Some compute -> compute
2278  initializer
2279   compute_ref <-
2280    Some (lazy (
2281    let scrolled_window1 =
2282     GBin.scrolled_window ~border_width:10
2283      ~packing:(vbox1#pack ~expand:true ~padding:5) () in
2284    let proofw =
2285     GMathView.math_view ~width:400 ~height:275
2286      ~packing:(scrolled_window1#add) () in
2287    let _ = proofw_ref <- Some proofw in
2288    let hbox3 =
2289     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
2290    let exactb =
2291     GButton.button ~label:"Exact"
2292      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2293    let introsb =
2294     GButton.button ~label:"Intros"
2295      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2296    let applyb =
2297     GButton.button ~label:"Apply"
2298      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2299    let elimsimplintrosb =
2300     GButton.button ~label:"ElimSimplIntros"
2301      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2302    let elimtypeb =
2303     GButton.button ~label:"ElimType"
2304      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2305    let whdb =
2306     GButton.button ~label:"Whd"
2307      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2308    let reduceb =
2309     GButton.button ~label:"Reduce"
2310      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2311    let simplb =
2312     GButton.button ~label:"Simpl"
2313      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2314    let foldb =
2315     GButton.button ~label:"Fold"
2316      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2317    let cutb =
2318     GButton.button ~label:"Cut"
2319      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2320    let hbox4 =
2321     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
2322    let changeb =
2323     GButton.button ~label:"Change"
2324      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2325    let letinb =
2326     GButton.button ~label:"Let ... In"
2327      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2328    let ringb =
2329     GButton.button ~label:"Ring"
2330      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2331    let clearbodyb =
2332     GButton.button ~label:"ClearBody"
2333      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2334    let clearb =
2335     GButton.button ~label:"Clear"
2336      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2337    let fourierb =
2338     GButton.button ~label:"Fourier"
2339      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2340    let rewritesimplb =
2341     GButton.button ~label:"RewriteSimpl ->"
2342      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2343    let reflexivityb =
2344     GButton.button ~label:"Reflexivity"
2345      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2346    let hbox5 =
2347     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
2348    let symmetryb =
2349     GButton.button ~label:"Symmetry"
2350      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2351    let transitivityb =
2352     GButton.button ~label:"Transitivity"
2353      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2354    let existsb =
2355     GButton.button ~label:"Exists"
2356      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2357    let splitb =
2358     GButton.button ~label:"Split"
2359      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2360    let leftb =
2361     GButton.button ~label:"Left"
2362      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2363    let rightb =
2364     GButton.button ~label:"Right"
2365      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2366    let assumptionb =
2367     GButton.button ~label:"Assumption"
2368      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2369    let generalizeb =
2370     GButton.button ~label:"Generalize"
2371      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2372    let hbox6 =
2373     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
2374    let absurdb =
2375     GButton.button ~label:"Absurd"
2376      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
2377    let contradictionb =
2378     GButton.button ~label:"Contradiction"
2379      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
2380    let searchpatternb =
2381     GButton.button ~label:"SearchPattern_Apply"
2382      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
2383
2384    ignore(exactb#connect#clicked exact) ;
2385    ignore(applyb#connect#clicked apply) ;
2386    ignore(elimsimplintrosb#connect#clicked elimsimplintros) ;
2387    ignore(elimtypeb#connect#clicked elimtype) ;
2388    ignore(whdb#connect#clicked whd) ;
2389    ignore(reduceb#connect#clicked reduce) ;
2390    ignore(simplb#connect#clicked simpl) ;
2391    ignore(foldb#connect#clicked fold) ;
2392    ignore(cutb#connect#clicked cut) ;
2393    ignore(changeb#connect#clicked change) ;
2394    ignore(letinb#connect#clicked letin) ;
2395    ignore(ringb#connect#clicked ring) ;
2396    ignore(clearbodyb#connect#clicked clearbody) ;
2397    ignore(clearb#connect#clicked clear) ;
2398    ignore(fourierb#connect#clicked fourier) ;
2399    ignore(rewritesimplb#connect#clicked rewritesimpl) ;
2400    ignore(reflexivityb#connect#clicked reflexivity) ;
2401    ignore(symmetryb#connect#clicked symmetry) ;
2402    ignore(transitivityb#connect#clicked transitivity) ;
2403    ignore(existsb#connect#clicked exists) ;
2404    ignore(splitb#connect#clicked split) ;
2405    ignore(leftb#connect#clicked left) ;
2406    ignore(rightb#connect#clicked right) ;
2407    ignore(assumptionb#connect#clicked assumption) ;
2408    ignore(generalizeb#connect#clicked generalize) ;
2409    ignore(absurdb#connect#clicked absurd) ;
2410    ignore(contradictionb#connect#clicked contradiction) ;
2411    ignore(introsb#connect#clicked intros) ;
2412    ignore(searchpatternb#connect#clicked searchPattern) ;
2413    ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
2414   ))
2415 end
2416 ;;
2417
2418 class empty_page =
2419  let vbox1 = GPack.vbox () in
2420  let scrolled_window1 =
2421   GBin.scrolled_window ~border_width:10
2422    ~packing:(vbox1#pack ~expand:true ~padding:5) () in
2423  let proofw =
2424   GMathView.math_view ~width:400 ~height:275
2425    ~packing:(scrolled_window1#add) () in
2426 object(self)
2427  method proofw = (assert false : GMathView.math_view)
2428  method content = vbox1
2429  method compute = (assert false : unit)
2430 end
2431 ;;
2432
2433 let empty_page = new empty_page;;
2434
2435 class notebook =
2436 object(self)
2437  val notebook = GPack.notebook ()
2438  val pages = ref []
2439  val mutable skip_switch_page_event = false
2440  val mutable empty = true
2441  method notebook = notebook
2442  method add_page n =
2443   let new_page = new page () in
2444    empty <- false ;
2445    pages := !pages @ [n,lazy (setgoal n),new_page] ;
2446    notebook#append_page
2447     ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce)
2448     new_page#content#coerce
2449  method remove_all_pages ~skip_switch_page_event:skip =
2450   if empty then
2451    notebook#remove_page 0 (* let's remove the empty page *)
2452   else
2453    List.iter (function _ -> notebook#remove_page 0) !pages ;
2454   pages := [] ;
2455   skip_switch_page_event <- skip
2456  method set_current_page ~may_skip_switch_page_event n =
2457   let (_,_,page) = List.find (function (m,_,_) -> m=n) !pages in
2458    let new_page = notebook#page_num page#content#coerce in
2459     if may_skip_switch_page_event && new_page <> notebook#current_page then
2460      skip_switch_page_event <- true ;
2461     notebook#goto_page new_page
2462  method set_empty_page =
2463   empty <- true ;
2464   pages := [] ;
2465   notebook#append_page
2466    ~tab_label:((GMisc.label ~text:"No proof in progress" ())#coerce)
2467    empty_page#content#coerce
2468  method proofw =
2469   let (_,_,page) = List.nth !pages notebook#current_page in
2470    page#proofw
2471  initializer
2472   ignore
2473    (notebook#connect#switch_page
2474     (function i ->
2475       let skip = skip_switch_page_event in
2476        skip_switch_page_event <- false ;
2477        if not skip then
2478         try
2479          let (metano,setgoal,page) = List.nth !pages i in
2480           ProofEngine.goal := Some metano ;
2481           Lazy.force (page#compute) ;
2482           Lazy.force setgoal
2483         with _ -> ()
2484     ))
2485 end
2486 ;;
2487
2488 (* Main window *)
2489
2490 class rendering_window output (notebook : notebook) =
2491  let scratch_window = new scratch_window in
2492  let window =
2493   GWindow.window ~title:"MathML viewer" ~border_width:0
2494    ~allow_shrink:false () in
2495  let vbox_for_menu = GPack.vbox ~packing:window#add () in
2496  (* menus *)
2497  let handle_box = GBin.handle_box ~border_width:2
2498   ~packing:(vbox_for_menu#pack ~padding:0) () in
2499  let menubar = GMenu.menu_bar ~packing:handle_box#add () in
2500  let factory0 = new GMenu.factory menubar in
2501  let accel_group = factory0#accel_group in
2502  (* file menu *)
2503  let file_menu = factory0#add_submenu "File" in
2504  let factory1 = new GMenu.factory file_menu ~accel_group in
2505  let export_to_postscript_menu_item =
2506   begin
2507    let _ =
2508     factory1#add_item "New Proof or Definition..." ~key:GdkKeysyms._N
2509      ~callback:new_proof
2510    in
2511    let reopen_menu_item =
2512     factory1#add_item "Reopen a Finished Proof..." ~key:GdkKeysyms._R
2513      ~callback:open_
2514    in
2515    let qed_menu_item =
2516     factory1#add_item "Qed" ~key:GdkKeysyms._E ~callback:qed in
2517    ignore (factory1#add_separator ()) ;
2518    ignore
2519     (factory1#add_item "Load Unfinished Proof..." ~key:GdkKeysyms._L
2520       ~callback:load) ;
2521    let save_menu_item =
2522     factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S ~callback:save
2523    in
2524    ignore
2525     (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b);
2526    ignore (!save_set_sensitive false);
2527    ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b);
2528    ignore (!qed_set_sensitive false);
2529    ignore (factory1#add_separator ()) ;
2530    let export_to_postscript_menu_item =
2531     factory1#add_item "Export to PostScript..."
2532      ~callback:(export_to_postscript output) in
2533    ignore (factory1#add_separator ()) ;
2534    ignore
2535     (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) ;
2536    export_to_postscript_menu_item
2537   end in
2538  (* edit menu *)
2539  let edit_menu = factory0#add_submenu "Edit Current Proof" in
2540  let factory2 = new GMenu.factory edit_menu ~accel_group in
2541  let focus_and_proveit_set_sensitive = ref (function _ -> assert false) in
2542  let proveit_menu_item =
2543   factory2#add_item "Prove It" ~key:GdkKeysyms._I
2544    ~callback:(function () -> proveit ();!focus_and_proveit_set_sensitive false)
2545  in
2546  let focus_menu_item =
2547   factory2#add_item "Focus" ~key:GdkKeysyms._F
2548    ~callback:(function () -> focus () ; !focus_and_proveit_set_sensitive false)
2549  in
2550  let _ =
2551   focus_and_proveit_set_sensitive :=
2552    function b ->
2553     proveit_menu_item#misc#set_sensitive b ;
2554     focus_menu_item#misc#set_sensitive b
2555  in
2556  let _ = !focus_and_proveit_set_sensitive false in
2557  (* edit term menu *)
2558  let edit_term_menu = factory0#add_submenu "Edit Term" in
2559  let factory5 = new GMenu.factory edit_term_menu ~accel_group in
2560  let check_menu_item =
2561   factory5#add_item "Check Term" ~key:GdkKeysyms._C
2562    ~callback:(check scratch_window) in
2563  let _ = check_menu_item#misc#set_sensitive false in
2564  (* search menu *)
2565  let settings_menu = factory0#add_submenu "Search" in
2566  let factory4 = new GMenu.factory settings_menu ~accel_group in
2567  let _ =
2568   factory4#add_item "Locate..." ~key:GdkKeysyms._T
2569    ~callback:locate in
2570  let show_menu_item =
2571   factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show
2572  in
2573  (* settings menu *)
2574  let settings_menu = factory0#add_submenu "Settings" in
2575  let factory3 = new GMenu.factory settings_menu ~accel_group in
2576  let _ =
2577   factory3#add_item "Edit Aliases" ~key:GdkKeysyms._A
2578    ~callback:edit_aliases in
2579  let _ = factory3#add_separator () in
2580  let _ =
2581   factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P
2582    ~callback:(function _ -> (settings_window ())#show ()) in
2583  (* accel group *)
2584  let _ = window#add_accel_group accel_group in
2585  (* end of menus *)
2586  let hbox0 =
2587   GPack.hbox
2588    ~packing:(vbox_for_menu#pack ~expand:true ~fill:true ~padding:5) () in
2589  let vbox =
2590   GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
2591  let scrolled_window0 =
2592   GBin.scrolled_window ~border_width:10
2593    ~packing:(vbox#pack ~expand:true ~padding:5) () in
2594  let _ = scrolled_window0#add output#coerce in
2595  let frame =
2596   GBin.frame ~label:"Insert Term"
2597    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2598  let scrolled_window1 =
2599   GBin.scrolled_window ~border_width:5
2600    ~packing:frame#add () in
2601  let inputt =
2602   new term_editor ~width:400 ~height:100 ~packing:scrolled_window1#add ()
2603    ~isnotempty_callback:check_menu_item#misc#set_sensitive in
2604  let vboxl =
2605   GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
2606  let _ =
2607   vboxl#pack ~expand:true ~fill:true ~padding:5 notebook#notebook#coerce in
2608  let frame =
2609   GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
2610  in
2611  let outputhtml =
2612   GHtml.xmhtml
2613    ~source:"<html><body bgColor=\"white\"></body></html>"
2614    ~width:400 ~height: 100
2615    ~border_width:20
2616    ~packing:frame#add
2617    ~show:true () in
2618 object
2619  method outputhtml = outputhtml
2620  method inputt = inputt
2621  method output = (output : GMathView.math_view)
2622  method notebook = notebook
2623  method show = window#show
2624  initializer
2625   notebook#set_empty_page ;
2626   export_to_postscript_menu_item#misc#set_sensitive false ;
2627   check_term := (check_term_in_scratch scratch_window) ;
2628
2629   (* signal handlers here *)
2630   ignore(output#connect#selection_changed
2631    (function elem ->
2632      choose_selection output elem ;
2633      !focus_and_proveit_set_sensitive true
2634    )) ;
2635   ignore (output#connect#clicked (show_in_show_window_callback output)) ;
2636   let settings_window = new settings_window output scrolled_window0
2637    export_to_postscript_menu_item (choose_selection output) in
2638   set_settings_window settings_window ;
2639   set_outputhtml outputhtml ;
2640   ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
2641   Logger.log_callback :=
2642    (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
2643 end;;
2644
2645 (* MAIN *)
2646
2647 let initialize_everything () =
2648  let module U = Unix in
2649   let output = GMathView.math_view ~width:350 ~height:280 () in
2650   let notebook = new notebook in
2651    let rendering_window' = new rendering_window output notebook in
2652     set_rendering_window rendering_window' ;
2653     mml_of_cic_term_ref := mml_of_cic_term ;
2654     rendering_window'#show () ;
2655     GMain.Main.main ()
2656 ;;
2657
2658 let _ =
2659  if !usedb then
2660 (*<<<<<<< gTopLevel.ml
2661 (* Mqint.init "dbname=helm_mowgli" ; *)
2662 Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ;
2663 =======*)
2664   begin
2665    Mqint.set_database Mqint.postgres_db ;
2666    (* Mqint.init "dbname=helm_mowgli" ; *)
2667    (* Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ; *)
2668    Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm" ;
2669   end ;
2670 (*>>>>>>> 1.35.2.34*)
2671  ignore (GtkMain.Main.init ()) ;
2672  initialize_everything () ;
2673  if !usedb then Mqint.close ();
2674 ;;