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 (* GLOBAL CONSTANTS *)
  38
  39 let helmns = Gdome.domString "http://www.cs.unibo.it/helm";;
  40 let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
  41
  42 let htmlheader =
  43  "<html>" ^
  44  " <body bgColor=\"white\">"
  45 ;;
  46
  47 let htmlfooter =
  48  " </body>" ^
  49  "</html>"
  50 ;;
  51
  52 let prooffile =
  53  try
  54   Sys.getenv "GTOPLEVEL_PROOFFILE"
  55  with
  56   Not_found -> "/public/currentproof"
  57 ;;
  58
  59 let prooffiletype =
  60  try
  61   Sys.getenv "GTOPLEVEL_PROOFFILETYPE"
  62  with
  63   Not_found -> "/public/currentprooftype"
  64 ;;
  65
  66 (*CSC: the getter should handle the innertypes, not the FS *)
  67
  68 let innertypesfile =
  69  try
  70   Sys.getenv "GTOPLEVEL_INNERTYPESFILE"
  71  with
  72   Not_found -> "/public/innertypes"
  73 ;;
  74
  75 let constanttypefile =
  76  try
  77   Sys.getenv "GTOPLEVEL_CONSTANTTYPEFILE"
  78  with
  79   Not_found -> "/public/constanttype"
  80 ;;
  81
  82 let postgresqlconnectionstring =
  83  try
  84   Sys.getenv "POSTGRESQL_CONNECTION_STRING"
  85  with
  86   Not_found -> "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm"
  87 ;;
  88
  89 let empty_id_to_uris = ([],function _ -> None);;
  90
  91
  92 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
  93
  94 let htmlheader_and_content = ref htmlheader;;
  95
  96 let current_cic_infos = ref None;;
  97 let current_goal_infos = ref None;;
  98 let current_scratch_infos = ref None;;
  99
 100 let id_to_uris = ref empty_id_to_uris;;
 101
 102 let check_term = ref (fun _ _ _ -> assert false);;
 103 let mml_of_cic_term_ref = ref (fun _ _ -> assert false);;
 104
 105 exception RenderingWindowsNotInitialized;;
 106
 107 let set_rendering_window,rendering_window =
 108  let rendering_window_ref = ref None in
 109   (function rw -> rendering_window_ref := Some rw),
 110   (function () ->
 111     match !rendering_window_ref with
 112        None -> raise RenderingWindowsNotInitialized
 113      | Some rw -> rw
 114   )
 115 ;;
 116
 117 exception SettingsWindowsNotInitialized;;
 118
 119 let set_settings_window,settings_window =
 120  let settings_window_ref = ref None in
 121   (function rw -> settings_window_ref := Some rw),
 122   (function () ->
 123     match !settings_window_ref with
 124        None -> raise SettingsWindowsNotInitialized
 125      | Some rw -> rw
 126   )
 127 ;;
 128
 129 exception OutputHtmlNotInitialized;;
 130
 131 let set_outputhtml,outputhtml =
 132  let outputhtml_ref = ref None in
 133   (function rw -> outputhtml_ref := Some rw),
 134   (function () ->
 135     match !outputhtml_ref with
 136        None -> raise OutputHtmlNotInitialized
 137      | Some outputhtml -> outputhtml
 138   )
 139 ;;
 140
 141 exception QedSetSensitiveNotInitialized;;
 142 let qed_set_sensitive =
 143  ref (function _ -> raise QedSetSensitiveNotInitialized)
 144 ;;
 145
 146 exception SaveSetSensitiveNotInitialized;;
 147 let save_set_sensitive =
 148  ref (function _ -> raise SaveSetSensitiveNotInitialized)
 149 ;;
 150
 151 (* COMMAND LINE OPTIONS *)
 152
 153 let usedb = ref true
 154
 155 let argspec =
 156   [
 157     "-nodb", Arg.Clear usedb, "disable use of MathQL DB"
 158   ]
 159 in
 160 Arg.parse argspec ignore ""
 161
 162 (* MISC FUNCTIONS *)
 163
 164 let term_of_cic_textual_parser_uri uri =
 165  let module C = Cic in
 166  let module CTP = CicTextualParser0 in
 167   match uri with
 168      CTP.ConUri uri -> C.Const (uri,[])
 169    | CTP.VarUri uri -> C.Var (uri,[])
 170    | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[])
 171    | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[])
 172 ;;
 173
 174 let string_of_cic_textual_parser_uri uri =
 175  let module C = Cic in
 176  let module CTP = CicTextualParser0 in
 177   let uri' =
 178    match uri with
 179       CTP.ConUri uri -> UriManager.string_of_uri uri
 180     | CTP.VarUri uri -> UriManager.string_of_uri uri
 181     | CTP.IndTyUri (uri,tyno) ->
 182        UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1)
 183     | CTP.IndConUri (uri,tyno,consno) ->
 184        UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^
 185         string_of_int consno
 186   in
 187    (* 4 = String.length "cic:" *)
 188    String.sub uri' 4 (String.length uri' - 4)
 189 ;;
 190
 191 let output_html outputhtml msg =
 192  htmlheader_and_content := !htmlheader_and_content ^ msg ;
 193  outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
 194  outputhtml#set_topline (-1)
 195 ;;
 196
 197 (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *)
 198
 199 (* Check window *)
 200
 201 let check_window outputhtml uris =
 202  let window =
 203   GWindow.window
 204    ~width:800 ~modal:true ~title:"Check" ~border_width:2 () in
 205  let notebook =
 206   GPack.notebook ~scrollable:true ~packing:window#add () in
 207  window#show () ;
 208  let render_terms =
 209   List.map
 210    (function uri ->
 211      let scrolled_window =
 212       GBin.scrolled_window ~border_width:10
 213        ~packing:
 214          (notebook#append_page ~tab_label:((GMisc.label ~text:uri ())#coerce))
 215        ()
 216      in
 217       lazy
 218        (let mmlwidget =
 219          GMathViewAux.single_selection_math_view
 220           ~packing:scrolled_window#add ~width:400 ~height:280 () in
 221         let expr =
 222          let term =
 223           term_of_cic_textual_parser_uri
 224            (Disambiguate.cic_textual_parser_uri_of_string uri)
 225          in
 226           (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term))
 227         in
 228          try
 229           let mml = !mml_of_cic_term_ref 111 expr in
 230            mmlwidget#load_doc ~dom:mml
 231          with
 232           e ->
 233            output_html outputhtml
 234             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 235        )
 236    ) uris
 237  in
 238   ignore
 239    (notebook#connect#switch_page
 240      (function i -> Lazy.force (List.nth render_terms i)))
 241 ;;
 242
 243 exception NoChoice;;
 244
 245 let
 246  interactive_user_uri_choice ~(selection_mode:[`SINGLE|`EXTENDED]) ?(ok="Ok")
 247   ?(enable_button_for_non_vars=false) ~title ~msg uris
 248 =
 249  let choices = ref [] in
 250  let chosen = ref false in
 251  let use_only_constants = ref false in
 252  let window =
 253   GWindow.dialog ~modal:true ~title ~width:600 () in
 254  let lMessage =
 255   GMisc.label ~text:msg
 256    ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
 257  let scrolled_window =
 258   GBin.scrolled_window ~border_width:10
 259    ~packing:(window#vbox#pack ~expand:true ~fill:true ~padding:5) () in
 260  let clist =
 261   let expected_height = 18 * List.length uris in
 262    let height = if expected_height > 400 then 400 else expected_height in
 263     GList.clist ~columns:1 ~packing:scrolled_window#add
 264      ~height ~selection_mode:(selection_mode :> Gtk.Tags.selection_mode) () in
 265  let _ = List.map (function x -> clist#append [x]) uris in
 266  let hbox2 =
 267   GPack.hbox ~border_width:0
 268    ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
 269  let explain_label =
 270   GMisc.label ~text:"None of the above. Try this one:"
 271    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
 272  let manual_input =
 273   GEdit.entry ~editable:true
 274    ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
 275  let hbox =
 276   GPack.hbox ~border_width:0 ~packing:window#action_area#add () in
 277  let okb =
 278   GButton.button ~label:ok
 279    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 280  let _ = okb#misc#set_sensitive false in
 281  let nonvarsb =
 282   GButton.button
 283    ~packing:
 284     (function w ->
 285       if enable_button_for_non_vars then
 286        hbox#pack ~expand:false ~fill:false ~padding:5 w)
 287    ~label:"Try constants only" () in
 288  let checkb =
 289   GButton.button ~label:"Check"
 290    ~packing:(hbox#pack ~padding:5) () in
 291  let _ = checkb#misc#set_sensitive false in
 292  let cancelb =
 293   GButton.button ~label:"Abort"
 294    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 295  (* actions *)
 296  let check_callback () =
 297   assert (List.length !choices > 0) ;
 298   check_window (outputhtml ()) !choices
 299  in
 300   ignore (window#connect#destroy GMain.Main.quit) ;
 301   ignore (cancelb#connect#clicked window#destroy) ;
 302   ignore
 303    (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
 304   ignore
 305    (nonvarsb#connect#clicked
 306      (function () ->
 307        use_only_constants := true ;
 308        chosen := true ;
 309        window#destroy ()
 310    )) ;
 311   ignore (checkb#connect#clicked check_callback) ;
 312   ignore
 313    (clist#connect#select_row
 314      (fun ~row ~column ~event ->
 315        checkb#misc#set_sensitive true ;
 316        okb#misc#set_sensitive true ;
 317        choices := (List.nth uris row)::!choices)) ;
 318   ignore
 319    (clist#connect#unselect_row
 320      (fun ~row ~column ~event ->
 321        choices :=
 322         List.filter (function uri -> uri != (List.nth uris row)) !choices)) ;
 323   ignore
 324    (manual_input#connect#changed
 325      (fun _ ->
 326        if manual_input#text = "" then
 327         begin
 328          choices := [] ;
 329          checkb#misc#set_sensitive false ;
 330          okb#misc#set_sensitive false ;
 331          clist#misc#set_sensitive true
 332         end
 333        else
 334         begin
 335          choices := [manual_input#text] ;
 336          clist#unselect_all () ;
 337          checkb#misc#set_sensitive true ;
 338          okb#misc#set_sensitive true ;
 339          clist#misc#set_sensitive false
 340         end));
 341   window#set_position `CENTER ;
 342   window#show () ;
 343   GMain.Main.main () ;
 344   if !chosen then
 345    if !use_only_constants then
 346     List.filter
 347      (function uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
 348      uris
 349    else
 350     if List.length !choices > 0 then !choices else raise NoChoice
 351   else
 352    raise NoChoice
 353 ;;
 354
 355 let interactive_interpretation_choice interpretations =
 356  let chosen = ref None in
 357  let window =
 358   GWindow.window
 359    ~modal:true ~title:"Ambiguous well-typed input." ~border_width:2 () in
 360  let vbox = GPack.vbox ~packing:window#add () in
 361  let lMessage =
 362   GMisc.label
 363    ~text:
 364     ("Ambiguous input since there are many well-typed interpretations." ^
 365      " Please, choose one of them.")
 366    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 367  let notebook =
 368   GPack.notebook ~scrollable:true
 369    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
 370  let _ =
 371   List.map
 372    (function interpretation ->
 373      let clist =
 374       let expected_height = 18 * List.length interpretation in
 375        let height = if expected_height > 400 then 400 else expected_height in
 376         GList.clist ~columns:2 ~packing:notebook#append_page ~height
 377          ~titles:["id" ; "URI"] ()
 378      in
 379       ignore
 380        (List.map
 381          (function (id,uri) ->
 382            let n = clist#append [id;uri] in
 383             clist#set_row ~selectable:false n
 384          ) interpretation
 385        ) ;
 386       clist#columns_autosize ()
 387    ) interpretations in
 388  let hbox =
 389   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 390  let okb =
 391   GButton.button ~label:"Ok"
 392    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 393  let cancelb =
 394   GButton.button ~label:"Abort"
 395    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 396  (* actions *)
 397  ignore (window#connect#destroy GMain.Main.quit) ;
 398  ignore (cancelb#connect#clicked window#destroy) ;
 399  ignore
 400   (okb#connect#clicked
 401     (function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
 402  window#set_position `CENTER ;
 403  window#show () ;
 404  GMain.Main.main () ;
 405  match !chosen with
 406     None -> raise NoChoice
 407   | Some n -> n
 408 ;;
 409
 410
 411 (* MISC FUNCTIONS *)
 412
 413 (* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
 414 let get_last_query =
 415  let query = ref "" in
 416   MQueryGenerator.set_confirm_query
 417    (function q -> query := MQueryUtil.text_of_query q ; true) ;
 418   function result -> !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
 419 ;;
 420
 421 let domImpl = Gdome.domImplementation ();;
 422
 423 let parseStyle name =
 424  let style =
 425   domImpl#createDocumentFromURI
 426 (*
 427    ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None
 428 *)
 429    ~uri:("styles/" ^ name) ()
 430  in
 431   Gdome_xslt.processStylesheet style
 432 ;;
 433
 434 let d_c = parseStyle "drop_coercions.xsl";;
 435 let tc1 = parseStyle "objtheorycontent.xsl";;
 436 let hc2 = parseStyle "content_to_html.xsl";;
 437 let l   = parseStyle "link.xsl";;
 438
 439 let c1 = parseStyle "rootcontent.xsl";;
 440 let g  = parseStyle "genmmlid.xsl";;
 441 let c2 = parseStyle "annotatedpres.xsl";;
 442
 443
 444 let getterURL = Configuration.getter_url;;
 445 let processorURL = Configuration.processor_url;;
 446
 447 let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
 448 let mml_args ~explode_all =
 449  ("explodeall",(if explode_all then "true()" else "false()"))::
 450   ["processorURL", "'" ^ processorURL ^ "'" ;
 451    "getterURL", "'" ^ getterURL ^ "'" ;
 452    "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
 453    "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
 454    "UNICODEvsSYMBOL", "'symbol'" ;
 455    "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
 456    "encoding", "'iso-8859-1'" ;
 457    "media-type", "'text/html'" ;
 458    "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
 459    "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
 460    "naturalLanguage", "'yes'" ;
 461    "annotations", "'no'" ;
 462    "URLs_or_URIs", "'URIs'" ;
 463    "topurl", "'http://phd.cs.unibo.it/helm'" ;
 464    "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
 465 ;;
 466
 467 let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
 468 let sequent_args =
 469  ["processorURL", "'" ^ processorURL ^ "'" ;
 470   "getterURL", "'" ^ getterURL ^ "'" ;
 471   "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
 472   "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
 473   "UNICODEvsSYMBOL", "'symbol'" ;
 474   "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
 475   "encoding", "'iso-8859-1'" ;
 476   "media-type", "'text/html'" ;
 477   "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
 478   "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
 479   "naturalLanguage", "'no'" ;
 480   "annotations", "'no'" ;
 481   "explodeall", "true()" ;
 482   "URLs_or_URIs", "'URIs'" ;
 483   "topurl", "'http://phd.cs.unibo.it/helm'" ;
 484   "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
 485 ;;
 486
 487 let parse_file filename =
 488  let inch = open_in filename in
 489   let rec read_lines () =
 490    try
 491     let line = input_line inch in
 492      line ^ read_lines ()
 493    with
 494     End_of_file -> ""
 495   in
 496    read_lines ()
 497 ;;
 498
 499 let applyStylesheets input styles args =
 500  List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
 501   input styles
 502 ;;
 503
 504 let
 505  mml_of_cic_object ~explode_all uri annobj ids_to_inner_sorts ids_to_inner_types
 506 =
 507 (*CSC: ????????????????? *)
 508  let xml, bodyxml =
 509   Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:true
 510    annobj
 511  in
 512  let xmlinnertypes =
 513   Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
 514    ~ask_dtd_to_the_getter:true
 515  in
 516   let input =
 517    match bodyxml with
 518       None -> Xml2Gdome.document_of_xml domImpl xml
 519     | Some bodyxml' ->
 520        Xml.pp xml (Some constanttypefile) ;
 521        Xml2Gdome.document_of_xml domImpl bodyxml'
 522   in
 523 (*CSC: We save the innertypes to disk so that we can retrieve them in the  *)
 524 (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
 525 (*CSC: local.                                                              *)
 526    Xml.pp xmlinnertypes (Some innertypesfile) ;
 527    let output = applyStylesheets input mml_styles (mml_args ~explode_all) in
 528     output
 529 ;;
 530
 531 let
 532  save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname
 533 =
 534  let name =
 535   let struri = UriManager.string_of_uri uri in
 536   let idx = (String.rindex struri '/') + 1 in
 537    String.sub struri idx (String.length struri - idx)
 538  in
 539   let path = pathname ^ "/" ^ name in
 540   let xml, bodyxml =
 541    Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false
 542     annobj
 543   in
 544   let xmlinnertypes =
 545    Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
 546     ~ask_dtd_to_the_getter:false
 547   in
 548    (* innertypes *)
 549    let innertypesuri = UriManager.innertypesuri_of_uri uri in
 550     Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ;
 551     Getter.register innertypesuri
 552      (Configuration.annotations_url ^
 553        Str.replace_first (Str.regexp "^cic:") ""
 554         (UriManager.string_of_uri innertypesuri) ^ ".xml"
 555      ) ;
 556     (* constant type / variable / mutual inductive types definition *)
 557     Xml.pp ~quiet:true xml (Some (path ^ ".xml")) ;
 558     Getter.register uri
 559      (Configuration.annotations_url ^
 560        Str.replace_first (Str.regexp "^cic:") ""
 561         (UriManager.string_of_uri uri) ^ ".xml"
 562      ) ;
 563     match bodyxml with
 564        None -> ()
 565      | Some bodyxml' ->
 566         (* constant body *)
 567         let bodyuri =
 568          match UriManager.bodyuri_of_uri uri with
 569             None -> assert false
 570           | Some bodyuri -> bodyuri
 571         in
 572          Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ;
 573          Getter.register bodyuri
 574           (Configuration.annotations_url ^
 575             Str.replace_first (Str.regexp "^cic:") ""
 576              (UriManager.string_of_uri bodyuri) ^ ".xml"
 577           )
 578 ;;
 579
 580
 581 (* CALLBACKS *)
 582
 583 exception RefreshSequentException of exn;;
 584 exception RefreshProofException of exn;;
 585
 586 let refresh_proof (output : GMathViewAux.single_selection_math_view) =
 587  try
 588   let uri,currentproof =
 589    match !ProofEngine.proof with
 590       None -> assert false
 591     | Some (uri,metasenv,bo,ty) ->
 592        !qed_set_sensitive (List.length metasenv = 0) ;
 593        (*CSC: Wrong: [] is just plainly wrong *)
 594        uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
 595   in
 596    let
 597     (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
 598      ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
 599    =
 600     Cic2acic.acic_object_of_cic_object currentproof
 601    in
 602     let mml =
 603      mml_of_cic_object ~explode_all:true uri acic ids_to_inner_sorts
 604       ids_to_inner_types
 605     in
 606      output#load_doc ~dom:mml ;
 607      current_cic_infos :=
 608       Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses)
 609  with
 610   e ->
 611  match !ProofEngine.proof with
 612     None -> assert false
 613   | Some (uri,metasenv,bo,ty) ->
 614 prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
 615    raise (RefreshProofException e)
 616 ;;
 617
 618 let refresh_sequent ?(empty_notebook=true) notebook =
 619  try
 620   match !ProofEngine.goal with
 621      None ->
 622       if empty_notebook then
 623        begin
 624         notebook#remove_all_pages ~skip_switch_page_event:false ;
 625         notebook#set_empty_page
 626        end
 627       else
 628        notebook#proofw#unload
 629    | Some metano ->
 630       let metasenv =
 631        match !ProofEngine.proof with
 632           None -> assert false
 633         | Some (_,metasenv,_,_) -> metasenv
 634       in
 635       let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
 636        let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
 637         SequentPp.XmlPp.print_sequent metasenv currentsequent
 638        in
 639         let regenerate_notebook () =
 640          let skip_switch_page_event =
 641           match metasenv with
 642              (m,_,_)::_ when m = metano -> false
 643            | _ -> true
 644          in
 645           notebook#remove_all_pages ~skip_switch_page_event ;
 646           List.iter (function (m,_,_) -> notebook#add_page m) metasenv ;
 647         in
 648           if empty_notebook then
 649            begin
 650             regenerate_notebook () ;
 651             notebook#set_current_page ~may_skip_switch_page_event:false metano
 652            end
 653           else
 654            begin
 655             let sequent_doc = Xml2Gdome.document_of_xml domImpl sequent_gdome in
 656             let sequent_mml =
 657              applyStylesheets sequent_doc sequent_styles sequent_args
 658             in
 659              notebook#set_current_page ~may_skip_switch_page_event:true metano;
 660              notebook#proofw#load_doc ~dom:sequent_mml
 661            end ;
 662           current_goal_infos :=
 663            Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
 664  with
 665   e ->
 666 let metano =
 667   match !ProofEngine.goal with
 668      None -> assert false
 669    | Some m -> m
 670 in
 671 let metasenv =
 672  match !ProofEngine.proof with
 673     None -> assert false
 674   | Some (_,metasenv,_,_) -> metasenv
 675 in
 676 try
 677 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
 678 prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
 679    raise (RefreshSequentException e)
 680 with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unkown."); raise (RefreshSequentException e)
 681 ;;
 682
 683 (*
 684 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
 685  ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ;
 686 *)
 687
 688 let mml_of_cic_term metano term =
 689  let metasenv =
 690   match !ProofEngine.proof with
 691      None -> []
 692    | Some (_,metasenv,_,_) -> metasenv
 693  in
 694  let context =
 695   match !ProofEngine.goal with
 696      None -> []
 697    | Some metano ->
 698       let (_,canonical_context,_) =
 699        List.find (function (m,_,_) -> m=metano) metasenv
 700       in
 701        canonical_context
 702  in
 703    let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
 704     SequentPp.XmlPp.print_sequent metasenv (metano,context,term)
 705    in
 706     let sequent_doc =
 707      Xml2Gdome.document_of_xml domImpl sequent_gdome
 708     in
 709      let res =
 710       applyStylesheets sequent_doc sequent_styles sequent_args ;
 711      in
 712       current_scratch_infos :=
 713        Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ;
 714       res
 715 ;;
 716
 717 exception OpenConjecturesStillThere;;
 718 exception WrongProof;;
 719
 720 let pathname_of_annuri uristring =
 721  Configuration.annotations_dir ^
 722   Str.replace_first (Str.regexp "^cic:") "" uristring
 723 ;;
 724
 725 let make_dirs dirpath =
 726  ignore (Unix.system ("mkdir -p " ^ dirpath))
 727 ;;
 728
 729 let save_obj uri obj =
 730  let
 731   (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
 732    ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
 733  =
 734   Cic2acic.acic_object_of_cic_object obj
 735  in
 736   (* let's save the theorem and register it to the getter *)
 737   let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
 738    make_dirs pathname ;
 739    save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
 740     pathname
 741 ;;
 742
 743 let qed () =
 744  match !ProofEngine.proof with
 745     None -> assert false
 746   | Some (uri,[],bo,ty) ->
 747      if
 748       CicReduction.are_convertible []
 749        (CicTypeChecker.type_of_aux' [] [] bo) ty
 750      then
 751       begin
 752        (*CSC: Wrong: [] is just plainly wrong *)
 753        let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in
 754         let
 755          (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
 756           ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
 757         =
 758          Cic2acic.acic_object_of_cic_object proof
 759         in
 760          let mml =
 761           mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts
 762            ids_to_inner_types
 763          in
 764           ((rendering_window ())#output : GMathViewAux.single_selection_math_view)#load_doc mml ;
 765           !qed_set_sensitive false ;
 766           (* let's save the theorem and register it to the getter *)
 767           let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
 768           make_dirs pathname ;
 769           save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
 770            pathname ;
 771           current_cic_infos :=
 772            Some
 773             (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
 774              ids_to_hypotheses)
 775       end
 776      else
 777       raise WrongProof
 778   | _ -> raise OpenConjecturesStillThere
 779 ;;
 780
 781 let save () =
 782  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
 783   match !ProofEngine.proof with
 784      None -> assert false
 785    | Some (uri, metasenv, bo, ty) ->
 786       let currentproof =
 787        (*CSC: Wrong: [] is just plainly wrong *)
 788        Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
 789       in
 790        let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
 791         Cic2acic.acic_object_of_cic_object currentproof
 792        in
 793         let xml, bodyxml =
 794          match
 795           Cic2Xml.print_object uri ~ids_to_inner_sorts
 796            ~ask_dtd_to_the_getter:true acurrentproof
 797          with
 798             xml,Some bodyxml -> xml,bodyxml
 799           | _,None -> assert false
 800         in
 801          Xml.pp ~quiet:true xml (Some prooffiletype) ;
 802          output_html outputhtml
 803           ("<h1 color=\"Green\">Current proof type saved to " ^
 804            prooffiletype ^ "</h1>") ;
 805          Xml.pp ~quiet:true bodyxml (Some prooffile) ;
 806          output_html outputhtml
 807           ("<h1 color=\"Green\">Current proof body saved to " ^
 808            prooffile ^ "</h1>")
 809 ;;
 810
 811 (* Used to typecheck the loaded proofs *)
 812 let typecheck_loaded_proof metasenv bo ty =
 813  let module T = CicTypeChecker in
 814   ignore (
 815    List.fold_left
 816     (fun metasenv ((_,context,ty) as conj) ->
 817       ignore (T.type_of_aux' metasenv context ty) ;
 818       metasenv @ [conj]
 819     ) [] metasenv) ;
 820   ignore (T.type_of_aux' metasenv [] ty) ;
 821   ignore (T.type_of_aux' metasenv [] bo)
 822 ;;
 823
 824 let load () =
 825  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
 826  let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
 827  let notebook = (rendering_window ())#notebook in
 828   try
 829    match
 830     GToolbox.input_string ~title:"Load Unfinished Proof" ~text:"/dummy.con"
 831      "Choose an URI:"
 832    with
 833       None -> raise NoChoice
 834     | Some uri0 ->
 835        let uri = UriManager.uri_of_string ("cic:" ^ uri0) in
 836         match CicParser.obj_of_xml prooffiletype (Some prooffile) with
 837            Cic.CurrentProof (_,metasenv,bo,ty,_) ->
 838             typecheck_loaded_proof metasenv bo ty ;
 839             ProofEngine.proof :=
 840              Some (uri, metasenv, bo, ty) ;
 841             ProofEngine.goal :=
 842              (match metasenv with
 843                  [] -> None
 844                | (metano,_,_)::_ -> Some metano
 845              ) ;
 846             refresh_proof output ;
 847             refresh_sequent notebook ;
 848              output_html outputhtml
 849               ("<h1 color=\"Green\">Current proof type loaded from " ^
 850                 prooffiletype ^ "</h1>") ;
 851              output_html outputhtml
 852               ("<h1 color=\"Green\">Current proof body loaded from " ^
 853                 prooffile ^ "</h1>") ;
 854             !save_set_sensitive true
 855          | _ -> assert false
 856   with
 857      RefreshSequentException e ->
 858       output_html outputhtml
 859        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 860         "sequent: " ^ Printexc.to_string e ^ "</h1>")
 861    | RefreshProofException e ->
 862       output_html outputhtml
 863        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 864         "proof: " ^ Printexc.to_string e ^ "</h1>")
 865    | e ->
 866       output_html outputhtml
 867        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 868 ;;
 869
 870 let edit_aliases () =
 871  let chosen = ref false in
 872  let window =
 873   GWindow.window
 874    ~width:400 ~modal:true ~title:"Edit Aliases..." ~border_width:2 () in
 875  let vbox =
 876   GPack.vbox ~border_width:0 ~packing:window#add () in
 877  let scrolled_window =
 878   GBin.scrolled_window ~border_width:10
 879    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
 880  let input = GEdit.text ~editable:true ~width:400 ~height:100
 881    ~packing:scrolled_window#add () in
 882  let hbox =
 883   GPack.hbox ~border_width:0
 884    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 885  let okb =
 886   GButton.button ~label:"Ok"
 887    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 888  let cancelb =
 889   GButton.button ~label:"Cancel"
 890    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 891  ignore (window#connect#destroy GMain.Main.quit) ;
 892  ignore (cancelb#connect#clicked window#destroy) ;
 893  ignore
 894   (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
 895  let dom,resolve_id = !id_to_uris in
 896   ignore
 897    (input#insert_text ~pos:0
 898     (String.concat "\n"
 899       (List.map
 900         (function v ->
 901           let uri =
 902            match resolve_id v with
 903               None -> assert false
 904             | Some uri -> uri
 905           in
 906            "alias " ^ v ^ " " ^
 907              (string_of_cic_textual_parser_uri uri)
 908         ) dom))) ;
 909   window#show () ;
 910   GMain.Main.main () ;
 911   if !chosen then
 912    let dom,resolve_id =
 913     let inputtext = input#get_chars 0 input#length in
 914     let regexpr =
 915      let alfa = "[a-zA-Z_-]" in
 916      let digit = "[0-9]" in
 917      let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in
 918      let blanks = "\( \|\t\|\n\)+" in
 919      let nonblanks = "[^ \t\n]+" in
 920      let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *)
 921       Str.regexp
 922        ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)")
 923     in
 924      let rec aux n =
 925       try
 926        let n' = Str.search_forward regexpr inputtext n in
 927         let id = Str.matched_group 2 inputtext in
 928         let uri =
 929          Disambiguate.cic_textual_parser_uri_of_string
 930           ("cic:" ^ (Str.matched_group 5 inputtext))
 931         in
 932          let dom,resolve_id = aux (n' + 1) in
 933           if List.mem id dom then
 934            dom,resolve_id
 935           else
 936            id::dom,
 937             (function id' -> if id = id' then Some uri else resolve_id id')
 938       with
 939        Not_found -> empty_id_to_uris
 940      in
 941       aux 0
 942    in
 943     id_to_uris := dom,resolve_id
 944 ;;
 945
 946 let proveit () =
 947  let module L = LogicalOperations in
 948  let module G = Gdome in
 949  let notebook = (rendering_window ())#notebook in
 950  let output = (rendering_window ())#output in
 951  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
 952   match (rendering_window ())#output#get_selection with
 953     Some node ->
 954      let xpath =
 955       ((node : Gdome.element)#getAttributeNS
 956       (*CSC: OCAML DIVERGE
 957       ((element : G.element)#getAttributeNS
 958       *)
 959         ~namespaceURI:helmns
 960         ~localName:(G.domString "xref"))#to_string
 961      in
 962       if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 963       else
 964        begin
 965         try
 966          match !current_cic_infos with
 967             Some (ids_to_terms, ids_to_father_ids, _, _) ->
 968              let id = xpath in
 969               L.to_sequent id ids_to_terms ids_to_father_ids ;
 970               refresh_proof output ;
 971               refresh_sequent notebook
 972           | None -> assert false (* "ERROR: No current term!!!" *)
 973         with
 974            RefreshSequentException e ->
 975             output_html outputhtml
 976              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 977               "sequent: " ^ Printexc.to_string e ^ "</h1>")
 978          | RefreshProofException e ->
 979             output_html outputhtml
 980              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 981               "proof: " ^ Printexc.to_string e ^ "</h1>")
 982          | e ->
 983             output_html outputhtml
 984              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 985        end
 986   | None -> assert false (* "ERROR: No selection!!!" *)
 987 ;;
 988
 989 let focus () =
 990  let module L = LogicalOperations in
 991  let module G = Gdome in
 992  let notebook = (rendering_window ())#notebook in
 993  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
 994   match (rendering_window ())#output#get_selection with
 995     Some node ->
 996      let xpath =
 997       ((node : Gdome.element)#getAttributeNS
 998       (*CSC: OCAML DIVERGE
 999       ((element : G.element)#getAttributeNS
1000       *)
1001         ~namespaceURI:helmns
1002         ~localName:(G.domString "xref"))#to_string
1003      in
1004       if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1005       else
1006        begin
1007         try
1008          match !current_cic_infos with
1009             Some (ids_to_terms, ids_to_father_ids, _, _) ->
1010              let id = xpath in
1011               L.focus id ids_to_terms ids_to_father_ids ;
1012               refresh_sequent notebook
1013           | None -> assert false (* "ERROR: No current term!!!" *)
1014         with
1015            RefreshSequentException e ->
1016             output_html outputhtml
1017              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1018               "sequent: " ^ Printexc.to_string e ^ "</h1>")
1019          | RefreshProofException e ->
1020             output_html outputhtml
1021              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1022               "proof: " ^ Printexc.to_string e ^ "</h1>")
1023          | e ->
1024             output_html outputhtml
1025              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1026        end
1027   | None -> assert false (* "ERROR: No selection!!!" *)
1028 ;;
1029
1030 exception NoPrevGoal;;
1031 exception NoNextGoal;;
1032
1033 let setgoal metano =
1034  let module L = LogicalOperations in
1035  let module G = Gdome in
1036  let notebook = (rendering_window ())#notebook in
1037  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1038   let metasenv =
1039    match !ProofEngine.proof with
1040       None -> assert false
1041     | Some (_,metasenv,_,_) -> metasenv
1042   in
1043    try
1044     refresh_sequent ~empty_notebook:false notebook
1045    with
1046       RefreshSequentException e ->
1047        output_html outputhtml
1048         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1049          "sequent: " ^ Printexc.to_string e ^ "</h1>")
1050     | e ->
1051        output_html outputhtml
1052         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1053 ;;
1054
1055 let
1056  show_in_show_window_obj, show_in_show_window_uri, show_in_show_window_callback
1057 =
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   GMathViewAux.single_selection_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_obj uri obj =
1067    let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1068     try
1069      let
1070       (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
1071        ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
1072      =
1073       Cic2acic.acic_object_of_cic_object obj
1074      in
1075       let mml =
1076        mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts
1077         ids_to_inner_types
1078       in
1079        window#set_title (UriManager.string_of_uri uri) ;
1080        window#misc#hide () ; window#show () ;
1081        mmlwidget#load_doc mml ;
1082     with
1083      e ->
1084       output_html outputhtml
1085        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1086   in
1087   let show_in_show_window_uri uri =
1088    let obj = CicEnvironment.get_obj uri in
1089     show_in_show_window_obj uri obj
1090   in
1091    let show_in_show_window_callback mmlwidget (n : Gdome.element) _ =
1092     if n#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then
1093      let uri =
1094       (n#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string
1095      in
1096       show_in_show_window_uri (UriManager.uri_of_string uri)
1097     else
1098      ignore (mmlwidget#action_toggle n)
1099    in
1100     let _ =
1101      mmlwidget#connect#click (show_in_show_window_callback mmlwidget)
1102     in
1103      show_in_show_window_obj, show_in_show_window_uri,
1104       show_in_show_window_callback
1105 ;;
1106
1107 exception NoObjectsLocated;;
1108
1109 let user_uri_choice ~title ~msg uris =
1110  let uri =
1111   match uris with
1112      [] -> raise NoObjectsLocated
1113    | [uri] -> uri
1114    | uris ->
1115       match
1116        interactive_user_uri_choice ~selection_mode:`SINGLE ~title ~msg uris
1117       with
1118          [uri] -> uri
1119        | _ -> assert false
1120  in
1121   String.sub uri 4 (String.length uri - 4)
1122 ;;
1123
1124 let locate_callback id =
1125  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1126  let result = MQueryGenerator.locate id in
1127  let uris =
1128   List.map
1129    (function uri,_ ->
1130      Disambiguate.wrong_xpointer_format_from_wrong_xpointer_format' uri)
1131    result in
1132  let html =
1133   (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>")
1134  in
1135   output_html outputhtml html ;
1136   user_uri_choice ~title:"Ambiguous input."
1137    ~msg:
1138      ("Ambiguous input \"" ^ id ^
1139       "\". Please, choose one interpetation:")
1140    uris
1141 ;;
1142
1143
1144 let input_or_locate_uri ~title =
1145  let uri = ref None in
1146  let window =
1147   GWindow.window
1148    ~width:400 ~modal:true ~title ~border_width:2 () in
1149  let vbox = GPack.vbox ~packing:window#add () in
1150  let hbox1 =
1151   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1152  let _ =
1153   GMisc.label ~text:"Enter a valid URI:" ~packing:(hbox1#pack ~padding:5) () in
1154  let manual_input =
1155   GEdit.entry ~editable:true
1156    ~packing:(hbox1#pack ~expand:true ~fill:true ~padding:5) () in
1157  let checkb =
1158   GButton.button ~label:"Check"
1159    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1160  let _ = checkb#misc#set_sensitive false in
1161  let hbox2 =
1162   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1163  let _ =
1164   GMisc.label ~text:"You can also enter an indentifier to locate:"
1165    ~packing:(hbox2#pack ~padding:5) () in
1166  let locate_input =
1167   GEdit.entry ~editable:true
1168    ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
1169  let locateb =
1170   GButton.button ~label:"Locate"
1171    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1172  let _ = locateb#misc#set_sensitive false in
1173  let hbox3 =
1174   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1175  let okb =
1176   GButton.button ~label:"Ok"
1177    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1178  let _ = okb#misc#set_sensitive false in
1179  let cancelb =
1180   GButton.button ~label:"Cancel"
1181    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) ()
1182  in
1183   ignore (window#connect#destroy GMain.Main.quit) ;
1184   ignore
1185    (cancelb#connect#clicked (function () -> uri := None ; window#destroy ())) ;
1186   let check_callback () =
1187    let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1188    let uri = "cic:" ^ manual_input#text in
1189     try
1190       ignore (Getter.resolve (UriManager.uri_of_string uri)) ;
1191       output_html outputhtml "<h1 color=\"Green\">OK</h1>" ;
1192       true
1193     with
1194        Getter.Unresolved ->
1195         output_html outputhtml
1196          ("<h1 color=\"Red\">URI " ^ uri ^
1197           " does not correspond to any object.</h1>") ;
1198         false
1199      | UriManager.IllFormedUri _ ->
1200         output_html outputhtml
1201          ("<h1 color=\"Red\">URI " ^ uri ^ " is not well-formed.</h1>") ;
1202         false
1203      | e ->
1204         output_html outputhtml
1205          ("<h1 color=\"Red\">" ^ Printexc.to_string e ^ "</h1>") ;
1206         false
1207   in
1208   ignore
1209    (okb#connect#clicked
1210      (function () ->
1211        if check_callback () then
1212         begin
1213          uri := Some manual_input#text ;
1214          window#destroy ()
1215         end
1216    )) ;
1217   ignore (checkb#connect#clicked (function () -> ignore (check_callback ()))) ;
1218   ignore
1219    (manual_input#connect#changed
1220      (fun _ ->
1221        if manual_input#text = "" then
1222         begin
1223          checkb#misc#set_sensitive false ;
1224          okb#misc#set_sensitive false
1225         end
1226        else
1227         begin
1228          checkb#misc#set_sensitive true ;
1229          okb#misc#set_sensitive true
1230         end));
1231   ignore
1232    (locate_input#connect#changed
1233      (fun _ -> locateb#misc#set_sensitive (locate_input#text <> ""))) ;
1234   ignore
1235    (locateb#connect#clicked
1236      (function () ->
1237        let id = locate_input#text in
1238         manual_input#set_text (locate_callback id) ;
1239         locate_input#delete_text 0 (String.length id)
1240    )) ;
1241   window#show () ;
1242   GMain.Main.main () ;
1243   match !uri with
1244      None -> raise NoChoice
1245    | Some uri -> UriManager.uri_of_string ("cic:" ^ uri)
1246 ;;
1247
1248 exception AmbiguousInput;;
1249
1250 (* A WIDGET TO ENTER CIC TERMS *)
1251
1252 module Callbacks =
1253  struct
1254   let output_html msg = output_html (outputhtml ()) msg;;
1255   let interactive_user_uri_choice =
1256    fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id ->
1257     interactive_user_uri_choice ~selection_mode ?ok
1258      ?enable_button_for_non_vars ~title ~msg;;
1259   let interactive_interpretation_choice = interactive_interpretation_choice;;
1260   let input_or_locate_uri = input_or_locate_uri;;
1261  end
1262 ;;
1263
1264 module Disambiguate' = Disambiguate.Make(Callbacks);;
1265
1266 class term_editor ?packing ?width ?height ?isnotempty_callback () =
1267  let input = GEdit.text ~editable:true ?width ?height ?packing () in
1268  let _ =
1269   match isnotempty_callback with
1270      None -> ()
1271    | Some callback ->
1272       ignore(input#connect#changed (function () -> callback (input#length > 0)))
1273  in
1274 object(self)
1275  method coerce = input#coerce
1276  method reset =
1277   input#delete_text 0 input#length
1278  (* CSC: txt is now a string, but should be of type Cic.term *)
1279  method set_term txt =
1280   self#reset ;
1281   ignore ((input#insert_text txt) ~pos:0)
1282  (* CSC: this method should disappear *)
1283  method get_as_string =
1284   input#get_chars 0 input#length
1285  method get_metasenv_and_term ~context ~metasenv =
1286   let name_context =
1287    List.map
1288     (function
1289         Some (n,_) -> Some n
1290       | None -> None
1291     ) context
1292   in
1293    let lexbuf = Lexing.from_string (input#get_chars 0 input#length) in
1294     let dom,mk_metasenv_and_expr =
1295      CicTextualParserContext.main
1296       ~context:name_context ~metasenv CicTextualLexer.token lexbuf
1297     in
1298      let id_to_uris',metasenv,expr =
1299       Disambiguate'.disambiguate_input context metasenv dom mk_metasenv_and_expr
1300        ~id_to_uris:!id_to_uris
1301      in
1302       id_to_uris := id_to_uris' ;
1303       metasenv,expr
1304 end
1305 ;;
1306
1307 (* OTHER FUNCTIONS *)
1308
1309 let locate () =
1310  let inputt = ((rendering_window ())#inputt : term_editor) in
1311  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1312    try
1313     match
1314      GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:"
1315     with
1316        None -> raise NoChoice
1317      | Some input ->
1318         let uri = locate_callback input in
1319          inputt#set_term uri
1320    with
1321     e ->
1322      output_html outputhtml
1323       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1324 ;;
1325
1326
1327 exception UriAlreadyInUse;;
1328 exception NotAUriToAConstant;;
1329
1330 let new_inductive () =
1331  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1332  let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
1333  let notebook = (rendering_window ())#notebook in
1334
1335  let chosen = ref false in
1336  let inductive = ref true in
1337  let paramsno = ref 0 in
1338  let get_uri = ref (function _ -> assert false) in
1339  let get_base_uri = ref (function _ -> assert false) in
1340  let get_names = ref (function _ -> assert false) in
1341  let get_types_and_cons = ref (function _ -> assert false) in
1342  let get_context_and_subst = ref (function _ -> assert false) in
1343  let window =
1344   GWindow.window
1345    ~width:600 ~modal:true ~position:`CENTER
1346    ~title:"New Block of Mutual (Co)Inductive Definitions"
1347    ~border_width:2 () in
1348  let vbox = GPack.vbox ~packing:window#add () in
1349  let hbox =
1350   GPack.hbox ~border_width:0
1351    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1352  let _ =
1353   GMisc.label ~text:"Enter the URI for the new block:"
1354    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1355  let uri_entry =
1356   GEdit.entry ~editable:true
1357    ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1358  let hbox0 =
1359   GPack.hbox ~border_width:0
1360    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1361  let _ =
1362   GMisc.label
1363    ~text:
1364      "Enter the number of left parameters in every arity and constructor type:"
1365    ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1366  let paramsno_entry =
1367   GEdit.entry ~editable:true ~text:"0"
1368    ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
1369  let hbox1 =
1370   GPack.hbox ~border_width:0
1371    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1372  let _ =
1373   GMisc.label ~text:"Are the definitions inductive or coinductive?"
1374    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1375  let inductiveb =
1376   GButton.radio_button ~label:"Inductive"
1377    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1378  let coinductiveb =
1379   GButton.radio_button ~label:"Coinductive"
1380    ~group:inductiveb#group
1381    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1382  let hbox2 =
1383   GPack.hbox ~border_width:0
1384    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1385  let _ =
1386   GMisc.label ~text:"Enter the list of the names of the types:"
1387    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1388  let names_entry =
1389   GEdit.entry ~editable:true
1390    ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
1391  let hboxn =
1392   GPack.hbox ~border_width:0
1393    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1394  let okb =
1395   GButton.button ~label:"> Next"
1396    ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1397  let _ = okb#misc#set_sensitive true in
1398  let cancelb =
1399   GButton.button ~label:"Abort"
1400    ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1401  ignore (window#connect#destroy GMain.Main.quit) ;
1402  ignore (cancelb#connect#clicked window#destroy) ;
1403  (* First phase *)
1404  let rec phase1 () =
1405   ignore
1406    (okb#connect#clicked
1407      (function () ->
1408        try
1409         let uristr = "cic:" ^ uri_entry#text in
1410         let namesstr = names_entry#text in
1411         let paramsno' = int_of_string (paramsno_entry#text) in
1412          match Str.split (Str.regexp " +") namesstr with
1413             [] -> assert false
1414           | (he::tl) as names ->
1415              let uri = UriManager.uri_of_string (uristr ^ "/" ^ he ^ ".ind") in
1416               begin
1417                try
1418                 ignore (Getter.resolve uri) ;
1419                 raise UriAlreadyInUse
1420                with
1421                 Getter.Unresolved ->
1422                  get_uri := (function () -> uri) ;
1423                  get_names := (function () -> names) ;
1424                  inductive := inductiveb#active ;
1425                  paramsno := paramsno' ;
1426                  phase2 ()
1427               end
1428        with
1429         e ->
1430          output_html outputhtml
1431           ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1432      ))
1433  (* Second phase *)
1434  and phase2 () =
1435   let type_widgets =
1436    List.map
1437     (function name ->
1438       let frame =
1439        GBin.frame ~label:name
1440         ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
1441       let vbox = GPack.vbox ~packing:frame#add () in
1442       let hbox = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false) () in
1443       let _ =
1444        GMisc.label ~text:("Enter its type:")
1445         ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1446       let scrolled_window =
1447        GBin.scrolled_window ~border_width:5
1448         ~packing:(vbox#pack ~expand:true ~padding:0) () in
1449       let newinputt =
1450        new term_editor ~width:400 ~height:20 ~packing:scrolled_window#add ()
1451         ~isnotempty_callback:
1452          (function b ->
1453            (*non_empty_type := b ;*)
1454            okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*)
1455       in
1456       let hbox =
1457        GPack.hbox ~border_width:0
1458         ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1459       let _ =
1460        GMisc.label ~text:("Enter the list of its constructors:")
1461         ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1462       let cons_names_entry =
1463        GEdit.entry ~editable:true
1464         ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1465       (newinputt,cons_names_entry)
1466     ) (!get_names ())
1467   in
1468    vbox#remove hboxn#coerce ;
1469    let hboxn =
1470     GPack.hbox ~border_width:0
1471      ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1472    let okb =
1473     GButton.button ~label:"> Next"
1474      ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1475    let cancelb =
1476     GButton.button ~label:"Abort"
1477      ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1478    ignore (cancelb#connect#clicked window#destroy) ;
1479    ignore
1480     (okb#connect#clicked
1481       (function () ->
1482         try
1483          let names = !get_names () in
1484          let types_and_cons =
1485           List.map2
1486            (fun name (newinputt,cons_names_entry) ->
1487              let consnamesstr = cons_names_entry#text in
1488              let cons_names = Str.split (Str.regexp " +") consnamesstr in
1489              let metasenv,expr =
1490               newinputt#get_metasenv_and_term ~context:[] ~metasenv:[]
1491              in
1492               match metasenv with
1493                  [] -> expr,cons_names
1494                | _ -> raise AmbiguousInput
1495            ) names type_widgets
1496          in
1497           let uri = !get_uri () in
1498           let _ =
1499            (* Let's see if so far the definition is well-typed *)
1500            let params = [] in
1501            let paramsno = 0 in
1502            (* To test if the arities of the inductive types are well *)
1503            (* typed, we check the inductive block definition where   *)
1504            (* no constructor is given to each type.                  *)
1505            let tys =
1506             List.map2
1507              (fun name (ty,cons) -> (name, !inductive, ty, []))
1508              names types_and_cons
1509            in
1510             CicTypeChecker.typecheck_mutual_inductive_defs uri
1511              (tys,params,paramsno)
1512           in
1513            get_context_and_subst :=
1514             (function () ->
1515               let i = ref 0 in
1516                List.fold_left2
1517                 (fun (context,subst) name (ty,_) ->
1518                   let res =
1519                    (Some (Cic.Name name, Cic.Decl ty))::context,
1520                     (Cic.MutInd (uri,!i,[]))::subst
1521                   in
1522                    incr i ; res
1523                 ) ([],[]) names types_and_cons) ;
1524            let types_and_cons' =
1525             List.map2
1526              (fun name (ty,cons) -> (name, !inductive, ty, phase3 name cons))
1527              names types_and_cons
1528            in
1529             get_types_and_cons := (function () -> types_and_cons') ;
1530             chosen := true ;
1531             window#destroy ()
1532         with
1533          e ->
1534           output_html outputhtml
1535            ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1536       ))
1537  (* Third phase *)
1538  and phase3 name cons =
1539   let get_cons_types = ref (function () -> assert false) in
1540   let window2 =
1541    GWindow.window
1542     ~width:600 ~modal:true ~position:`CENTER
1543     ~title:(name ^ " Constructors")
1544     ~border_width:2 () in
1545   let vbox = GPack.vbox ~packing:window2#add () in
1546   let cons_type_widgets =
1547    List.map
1548     (function consname ->
1549       let hbox =
1550        GPack.hbox ~border_width:0
1551         ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1552       let _ =
1553        GMisc.label ~text:("Enter the type of " ^ consname ^ ":")
1554         ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1555       let scrolled_window =
1556        GBin.scrolled_window ~border_width:5
1557         ~packing:(vbox#pack ~expand:true ~padding:0) () in
1558       let newinputt =
1559        new term_editor ~width:400 ~height:20 ~packing:scrolled_window#add ()
1560         ~isnotempty_callback:
1561          (function b ->
1562            (* (*non_empty_type := b ;*)
1563            okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*) *)())
1564       in
1565        newinputt
1566     ) cons in
1567   let hboxn =
1568    GPack.hbox ~border_width:0
1569     ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1570   let okb =
1571    GButton.button ~label:"> Next"
1572     ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1573   let _ = okb#misc#set_sensitive true in
1574   let cancelb =
1575    GButton.button ~label:"Abort"
1576     ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1577   ignore (window2#connect#destroy GMain.Main.quit) ;
1578   ignore (cancelb#connect#clicked window2#destroy) ;
1579   ignore
1580    (okb#connect#clicked
1581      (function () ->
1582        try
1583         chosen := true ;
1584         let context,subst= !get_context_and_subst () in
1585         let cons_types =
1586          List.map2
1587           (fun name inputt ->
1588             let metasenv,expr =
1589              inputt#get_metasenv_and_term ~context ~metasenv:[]
1590             in
1591              match metasenv with
1592                 [] ->
1593                  let undebrujined_expr =
1594                   List.fold_left
1595                    (fun expr t -> CicSubstitution.subst t expr) expr subst
1596                  in
1597                   name, undebrujined_expr
1598               | _ -> raise AmbiguousInput
1599           ) cons cons_type_widgets
1600         in
1601          get_cons_types := (function () -> cons_types) ;
1602          window2#destroy ()
1603        with
1604         e ->
1605          output_html outputhtml
1606           ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1607      )) ;
1608   window2#show () ;
1609   GMain.Main.main () ;
1610   let okb_pressed = !chosen in
1611    chosen := false ;
1612    if (not okb_pressed) then
1613     begin
1614      window#destroy () ;
1615      assert false (* The control never reaches this point *)
1616     end
1617    else
1618     (!get_cons_types ())
1619  in
1620   phase1 () ;
1621   (* No more phases left or Abort pressed *)
1622   window#show () ;
1623   GMain.Main.main () ;
1624   window#destroy () ;
1625   if !chosen then
1626    try
1627     let uri = !get_uri () in
1628 (*CSC: Da finire *)
1629     let params = [] in
1630     let tys = !get_types_and_cons () in
1631      let obj = Cic.InductiveDefinition tys params !paramsno in
1632       begin
1633        try
1634         prerr_endline (CicPp.ppobj obj) ;
1635         CicTypeChecker.typecheck_mutual_inductive_defs uri
1636          (tys,params,!paramsno) ;
1637         with
1638          e ->
1639           prerr_endline "Offending mutual (co)inductive type declaration:" ;
1640           prerr_endline (CicPp.ppobj obj) ;
1641       end ;
1642       (* We already know that obj is well-typed. We need to add it to the  *)
1643       (* environment in order to compute the inner-types without having to *)
1644       (* debrujin it or having to modify lots of other functions to avoid  *)
1645       (* asking the environment for the MUTINDs we are defining now.       *)
1646       CicEnvironment.put_inductive_definition uri obj ;
1647       save_obj uri obj ;
1648       show_in_show_window_obj uri obj
1649    with
1650     e ->
1651      output_html outputhtml
1652       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1653 ;;
1654
1655 let mk_fresh_name_callback context name ~typ =
1656  let fresh_name =
1657   match ProofEngineHelpers.mk_fresh_name context name ~typ with
1658      Cic.Name fresh_name -> fresh_name
1659    | Cic.Anonymous -> assert false
1660  in
1661   match
1662    GToolbox.input_string ~title:"Enter a fresh hypothesis name" ~text:fresh_name
1663     ("Enter a fresh name for the hypothesis " ^
1664       CicPp.pp typ
1665        (List.map (function None -> None | Some (n,_) -> Some n) context))
1666   with
1667      Some fresh_name' -> Cic.Name fresh_name'
1668    | None -> raise NoChoice
1669 ;;
1670
1671 let new_proof () =
1672  let inputt = ((rendering_window ())#inputt : term_editor) in
1673  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1674  let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
1675  let notebook = (rendering_window ())#notebook in
1676
1677  let chosen = ref false in
1678  let get_metasenv_and_term = ref (function _ -> assert false) in
1679  let get_uri = ref (function _ -> assert false) in
1680  let non_empty_type = ref false in
1681  let window =
1682   GWindow.window
1683    ~width:600 ~modal:true ~title:"New Proof or Definition"
1684    ~border_width:2 () in
1685  let vbox = GPack.vbox ~packing:window#add () in
1686  let hbox =
1687   GPack.hbox ~border_width:0
1688    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1689  let _ =
1690   GMisc.label ~text:"Enter the URI for the new theorem or definition:"
1691    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1692  let uri_entry =
1693   GEdit.entry ~editable:true
1694    ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1695  let hbox1 =
1696   GPack.hbox ~border_width:0
1697    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1698  let _ =
1699   GMisc.label ~text:"Enter the theorem or definition type:"
1700    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1701  let scrolled_window =
1702   GBin.scrolled_window ~border_width:5
1703    ~packing:(vbox#pack ~expand:true ~padding:0) () in
1704  (* the content of the scrolled_window is moved below (see comment) *)
1705  let hbox =
1706   GPack.hbox ~border_width:0
1707    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1708  let okb =
1709   GButton.button ~label:"Ok"
1710    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1711  let _ = okb#misc#set_sensitive false in
1712  let cancelb =
1713   GButton.button ~label:"Cancel"
1714    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1715  (* moved here to have visibility of the ok button *)
1716  let newinputt =
1717   new term_editor ~width:400 ~height:100 ~packing:scrolled_window#add ()
1718    ~isnotempty_callback:
1719     (function b ->
1720       non_empty_type := b ;
1721       okb#misc#set_sensitive (b && uri_entry#text <> ""))
1722  in
1723  let _ =
1724   newinputt#set_term inputt#get_as_string ;
1725   inputt#reset in
1726  let _ =
1727   uri_entry#connect#changed
1728    (function () ->
1729      okb#misc#set_sensitive (!non_empty_type && uri_entry#text <> ""))
1730  in
1731  ignore (window#connect#destroy GMain.Main.quit) ;
1732  ignore (cancelb#connect#clicked window#destroy) ;
1733  ignore
1734   (okb#connect#clicked
1735     (function () ->
1736       chosen := true ;
1737       try
1738        let metasenv,parsed = newinputt#get_metasenv_and_term [] [] in
1739        let uristr = "cic:" ^ uri_entry#text in
1740        let uri = UriManager.uri_of_string uristr in
1741         if String.sub uristr (String.length uristr - 4) 4 <> ".con" then
1742          raise NotAUriToAConstant
1743         else
1744          begin
1745           try
1746            ignore (Getter.resolve uri) ;
1747            raise UriAlreadyInUse
1748           with
1749            Getter.Unresolved ->
1750             get_metasenv_and_term := (function () -> metasenv,parsed) ;
1751             get_uri := (function () -> uri) ;
1752             window#destroy ()
1753          end
1754       with
1755        e ->
1756         output_html outputhtml
1757          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1758   )) ;
1759  window#show () ;
1760  GMain.Main.main () ;
1761  if !chosen then
1762   try
1763    let metasenv,expr = !get_metasenv_and_term () in
1764     let _  = CicTypeChecker.type_of_aux' metasenv [] expr in
1765      ProofEngine.proof :=
1766       Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
1767      ProofEngine.goal := Some 1 ;
1768      refresh_sequent notebook ;
1769      refresh_proof output ;
1770      !save_set_sensitive true ;
1771      inputt#reset ;
1772      ProofEngine.intros ~mk_fresh_name_callback () ;
1773      refresh_sequent notebook ;
1774      refresh_proof output
1775   with
1776      RefreshSequentException e ->
1777       output_html outputhtml
1778        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1779         "sequent: " ^ Printexc.to_string e ^ "</h1>")
1780    | RefreshProofException e ->
1781       output_html outputhtml
1782        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1783         "proof: " ^ Printexc.to_string e ^ "</h1>")
1784    | e ->
1785       output_html outputhtml
1786        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1787 ;;
1788
1789 let check_term_in_scratch scratch_window metasenv context expr =
1790  try
1791   let ty = CicTypeChecker.type_of_aux' metasenv context expr in
1792    let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
1793     scratch_window#show () ;
1794     scratch_window#mmlwidget#load_doc ~dom:mml
1795  with
1796   e ->
1797    print_endline ("? " ^ CicPp.ppterm expr) ;
1798    raise e
1799 ;;
1800
1801 let check scratch_window () =
1802  let inputt = ((rendering_window ())#inputt : term_editor) in
1803  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1804   let metasenv =
1805    match !ProofEngine.proof with
1806       None -> []
1807     | Some (_,metasenv,_,_) -> metasenv
1808   in
1809   let context =
1810    match !ProofEngine.goal with
1811       None -> []
1812     | Some metano ->
1813        let (_,canonical_context,_) =
1814         List.find (function (m,_,_) -> m=metano) metasenv
1815        in
1816         canonical_context
1817   in
1818    try
1819     let metasenv',expr = inputt#get_metasenv_and_term context metasenv in
1820      check_term_in_scratch scratch_window metasenv' context expr
1821    with
1822     e ->
1823      output_html outputhtml
1824       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1825 ;;
1826
1827 let decompose_uris_choice_callback uris =
1828 (* N.B.: in questo passaggio perdo l'informazione su exp_named_subst !!!! *)
1829   let module U = UriManager in
1830    List.map
1831     (function uri ->
1832       match Disambiguate.cic_textual_parser_uri_of_string uri with
1833          CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[])
1834        | _ -> assert false)
1835     (interactive_user_uri_choice
1836       ~selection_mode:`EXTENDED ~ok:"Ok" ~enable_button_for_non_vars:false
1837       ~title:"Decompose" ~msg:"Please, select the Inductive Types to decompose"
1838       (List.map
1839         (function (uri,typeno,_) ->
1840           U.string_of_uri uri ^ "#1/" ^ string_of_int (typeno+1)
1841         ) uris)
1842     )
1843 ;;
1844
1845 (***********************)
1846 (*       TACTICS       *)
1847 (***********************)
1848
1849 let call_tactic tactic () =
1850  let notebook = (rendering_window ())#notebook in
1851  let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
1852  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1853  let savedproof = !ProofEngine.proof in
1854  let savedgoal  = !ProofEngine.goal in
1855   begin
1856    try
1857     tactic () ;
1858     refresh_sequent notebook ;
1859     refresh_proof output
1860    with
1861       RefreshSequentException e ->
1862        output_html outputhtml
1863         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1864          "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1865        ProofEngine.proof := savedproof ;
1866        ProofEngine.goal := savedgoal ;
1867        refresh_sequent notebook
1868     | RefreshProofException e ->
1869        output_html outputhtml
1870         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1871          "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1872        ProofEngine.proof := savedproof ;
1873        ProofEngine.goal := savedgoal ;
1874        refresh_sequent notebook ;
1875        refresh_proof output
1876     | e ->
1877        output_html outputhtml
1878         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1879        ProofEngine.proof := savedproof ;
1880        ProofEngine.goal := savedgoal ;
1881   end
1882 ;;
1883
1884 let call_tactic_with_input tactic () =
1885  let notebook = (rendering_window ())#notebook in
1886  let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
1887  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1888  let inputt = ((rendering_window ())#inputt : term_editor) in
1889  let savedproof = !ProofEngine.proof in
1890  let savedgoal  = !ProofEngine.goal in
1891   let uri,metasenv,bo,ty =
1892    match !ProofEngine.proof with
1893       None -> assert false
1894     | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
1895   in
1896    let canonical_context =
1897     match !ProofEngine.goal with
1898        None -> assert false
1899      | Some metano ->
1900         let (_,canonical_context,_) =
1901          List.find (function (m,_,_) -> m=metano) metasenv
1902         in
1903          canonical_context
1904    in
1905     try
1906      let metasenv',expr =
1907       inputt#get_metasenv_and_term canonical_context metasenv
1908      in
1909       ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
1910       tactic expr ;
1911       refresh_sequent notebook ;
1912       refresh_proof output ;
1913       inputt#reset
1914     with
1915        RefreshSequentException e ->
1916         output_html outputhtml
1917          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1918           "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1919         ProofEngine.proof := savedproof ;
1920         ProofEngine.goal := savedgoal ;
1921         refresh_sequent notebook
1922      | RefreshProofException e ->
1923         output_html outputhtml
1924          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1925           "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1926         ProofEngine.proof := savedproof ;
1927         ProofEngine.goal := savedgoal ;
1928         refresh_sequent notebook ;
1929         refresh_proof output
1930      | e ->
1931         output_html outputhtml
1932          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1933         ProofEngine.proof := savedproof ;
1934         ProofEngine.goal := savedgoal ;
1935 ;;
1936
1937 let call_tactic_with_goal_input tactic () =
1938  let module L = LogicalOperations in
1939  let module G = Gdome in
1940   let notebook = (rendering_window ())#notebook in
1941   let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
1942   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1943   let savedproof = !ProofEngine.proof in
1944   let savedgoal  = !ProofEngine.goal in
1945    match notebook#proofw#get_selections with
1946      [node] ->
1947       let xpath =
1948        ((node : Gdome.element)#getAttributeNS
1949          ~namespaceURI:helmns
1950          ~localName:(G.domString "xref"))#to_string
1951       in
1952        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1953        else
1954         begin
1955          try
1956           match !current_goal_infos with
1957              Some (ids_to_terms, ids_to_father_ids,_) ->
1958               let id = xpath in
1959                tactic (Hashtbl.find ids_to_terms id) ;
1960                refresh_sequent notebook ;
1961                refresh_proof output
1962            | None -> assert false (* "ERROR: No current term!!!" *)
1963          with
1964             RefreshSequentException e ->
1965              output_html outputhtml
1966               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1967                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1968              ProofEngine.proof := savedproof ;
1969              ProofEngine.goal := savedgoal ;
1970              refresh_sequent notebook
1971           | RefreshProofException e ->
1972              output_html outputhtml
1973               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1974                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1975              ProofEngine.proof := savedproof ;
1976              ProofEngine.goal := savedgoal ;
1977              refresh_sequent notebook ;
1978              refresh_proof output
1979           | e ->
1980              output_html outputhtml
1981               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1982              ProofEngine.proof := savedproof ;
1983              ProofEngine.goal := savedgoal ;
1984         end
1985    | [] ->
1986       output_html outputhtml
1987        ("<h1 color=\"red\">No term selected</h1>")
1988    | _ ->
1989       output_html outputhtml
1990        ("<h1 color=\"red\">Many terms selected</h1>")
1991 ;;
1992
1993 let call_tactic_with_goal_inputs tactic () =
1994  let module L = LogicalOperations in
1995  let module G = Gdome in
1996   let notebook = (rendering_window ())#notebook in
1997   let output =
1998    ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
1999   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2000   let savedproof = !ProofEngine.proof in
2001   let savedgoal  = !ProofEngine.goal in
2002    try
2003     let term_of_node node =
2004      let xpath =
2005       ((node : Gdome.element)#getAttributeNS
2006         ~namespaceURI:helmns
2007         ~localName:(G.domString "xref"))#to_string
2008      in
2009       if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2010       else
2011        match !current_goal_infos with
2012           Some (ids_to_terms, ids_to_father_ids,_) ->
2013            let id = xpath in
2014             (Hashtbl.find ids_to_terms id)
2015         | None -> assert false (* "ERROR: No current term!!!" *)
2016     in
2017      match notebook#proofw#get_selections with
2018         [] ->
2019          output_html outputhtml
2020           ("<h1 color=\"red\">No term selected</h1>")
2021       | l ->
2022          let terms = List.map term_of_node l in
2023            match !current_goal_infos with
2024               Some (ids_to_terms, ids_to_father_ids,_) ->
2025                tactic terms ;
2026                refresh_sequent notebook ;
2027                refresh_proof output
2028             | None -> assert false (* "ERROR: No current term!!!" *)
2029    with
2030       RefreshSequentException e ->
2031        output_html outputhtml
2032         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2033          "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2034        ProofEngine.proof := savedproof ;
2035        ProofEngine.goal := savedgoal ;
2036        refresh_sequent notebook
2037     | RefreshProofException e ->
2038        output_html outputhtml
2039         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2040          "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2041        ProofEngine.proof := savedproof ;
2042        ProofEngine.goal := savedgoal ;
2043        refresh_sequent notebook ;
2044        refresh_proof output
2045     | e ->
2046        output_html outputhtml
2047         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2048        ProofEngine.proof := savedproof ;
2049        ProofEngine.goal := savedgoal
2050 ;;
2051
2052 let call_tactic_with_input_and_goal_input tactic () =
2053  let module L = LogicalOperations in
2054  let module G = Gdome in
2055   let notebook = (rendering_window ())#notebook in
2056   let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
2057   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2058   let inputt = ((rendering_window ())#inputt : term_editor) in
2059   let savedproof = !ProofEngine.proof in
2060   let savedgoal  = !ProofEngine.goal in
2061    match notebook#proofw#get_selections with
2062      [node] ->
2063       let xpath =
2064        ((node : Gdome.element)#getAttributeNS
2065          ~namespaceURI:helmns
2066          ~localName:(G.domString "xref"))#to_string
2067       in
2068        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2069        else
2070         begin
2071          try
2072           match !current_goal_infos with
2073              Some (ids_to_terms, ids_to_father_ids,_) ->
2074               let id = xpath in
2075                let uri,metasenv,bo,ty =
2076                 match !ProofEngine.proof with
2077                    None -> assert false
2078                  | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
2079                in
2080                 let canonical_context =
2081                  match !ProofEngine.goal with
2082                     None -> assert false
2083                   | Some metano ->
2084                      let (_,canonical_context,_) =
2085                       List.find (function (m,_,_) -> m=metano) metasenv
2086                      in
2087                       canonical_context in
2088                 let (metasenv',expr) =
2089                  inputt#get_metasenv_and_term canonical_context metasenv
2090                 in
2091                  ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
2092                  tactic ~goal_input:(Hashtbl.find ids_to_terms id)
2093                   ~input:expr ;
2094                  refresh_sequent notebook ;
2095                  refresh_proof output ;
2096                  inputt#reset
2097            | None -> assert false (* "ERROR: No current term!!!" *)
2098          with
2099             RefreshSequentException e ->
2100              output_html outputhtml
2101               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2102                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2103              ProofEngine.proof := savedproof ;
2104              ProofEngine.goal := savedgoal ;
2105              refresh_sequent notebook
2106           | RefreshProofException e ->
2107              output_html outputhtml
2108               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2109                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2110              ProofEngine.proof := savedproof ;
2111              ProofEngine.goal := savedgoal ;
2112              refresh_sequent notebook ;
2113              refresh_proof output
2114           | e ->
2115              output_html outputhtml
2116               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2117              ProofEngine.proof := savedproof ;
2118              ProofEngine.goal := savedgoal ;
2119         end
2120    | [] ->
2121       output_html outputhtml
2122        ("<h1 color=\"red\">No term selected</h1>")
2123    | _ ->
2124       output_html outputhtml
2125        ("<h1 color=\"red\">Many terms selected</h1>")
2126 ;;
2127
2128 let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
2129  let module L = LogicalOperations in
2130  let module G = Gdome in
2131   let mmlwidget =
2132    (scratch_window#mmlwidget : GMathViewAux.multi_selection_math_view) in
2133   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2134   let savedproof = !ProofEngine.proof in
2135   let savedgoal  = !ProofEngine.goal in
2136    match mmlwidget#get_selections with
2137      [node] ->
2138       let xpath =
2139        ((node : Gdome.element)#getAttributeNS
2140          ~namespaceURI:helmns
2141          ~localName:(G.domString "xref"))#to_string
2142       in
2143        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2144        else
2145         begin
2146          try
2147           match !current_scratch_infos with
2148              (* term is the whole goal in the scratch_area *)
2149              Some (term,ids_to_terms, ids_to_father_ids,_) ->
2150               let id = xpath in
2151                let expr = tactic term (Hashtbl.find ids_to_terms id) in
2152                 let mml = mml_of_cic_term 111 expr in
2153                  scratch_window#show () ;
2154                  scratch_window#mmlwidget#load_doc ~dom:mml
2155            | None -> assert false (* "ERROR: No current term!!!" *)
2156          with
2157           e ->
2158            output_html outputhtml
2159             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2160         end
2161    | [] ->
2162       output_html outputhtml
2163        ("<h1 color=\"red\">No term selected</h1>")
2164    | _ ->
2165       output_html outputhtml
2166        ("<h1 color=\"red\">Many terms selected</h1>")
2167 ;;
2168
2169 let call_tactic_with_goal_inputs_in_scratch tactic scratch_window () =
2170  let module L = LogicalOperations in
2171  let module G = Gdome in
2172   let mmlwidget =
2173    (scratch_window#mmlwidget : GMathViewAux.multi_selection_math_view) in
2174   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2175   let savedproof = !ProofEngine.proof in
2176   let savedgoal  = !ProofEngine.goal in
2177    match mmlwidget#get_selections with
2178       [] ->
2179        output_html outputhtml
2180         ("<h1 color=\"red\">No term selected</h1>")
2181     | l ->
2182        try
2183         match !current_scratch_infos with
2184            (* term is the whole goal in the scratch_area *)
2185            Some (term,ids_to_terms, ids_to_father_ids,_) ->
2186             let term_of_node node =
2187              let xpath =
2188               ((node : Gdome.element)#getAttributeNS
2189                 ~namespaceURI:helmns
2190                 ~localName:(G.domString "xref"))#to_string
2191              in
2192               if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2193               else
2194                let id = xpath in
2195                 Hashtbl.find ids_to_terms id
2196             in
2197              let terms = List.map term_of_node l in
2198               let expr = tactic terms term in
2199                let mml = mml_of_cic_term 111 expr in
2200                 scratch_window#show () ;
2201                 scratch_window#mmlwidget#load_doc ~dom:mml
2202          | None -> assert false (* "ERROR: No current term!!!" *)
2203        with
2204         e ->
2205          output_html outputhtml
2206           ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2207 ;;
2208
2209 let call_tactic_with_hypothesis_input tactic () =
2210  let module L = LogicalOperations in
2211  let module G = Gdome in
2212   let notebook = (rendering_window ())#notebook in
2213   let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
2214   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2215   let savedproof = !ProofEngine.proof in
2216   let savedgoal  = !ProofEngine.goal in
2217    match notebook#proofw#get_selections with
2218      [node] ->
2219       let xpath =
2220        ((node : Gdome.element)#getAttributeNS
2221          ~namespaceURI:helmns
2222          ~localName:(G.domString "xref"))#to_string
2223       in
2224        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2225        else
2226         begin
2227          try
2228           match !current_goal_infos with
2229              Some (_,_,ids_to_hypotheses) ->
2230               let id = xpath in
2231                tactic (Hashtbl.find ids_to_hypotheses id) ;
2232                refresh_sequent notebook ;
2233                refresh_proof output
2234            | None -> assert false (* "ERROR: No current term!!!" *)
2235          with
2236             RefreshSequentException e ->
2237              output_html outputhtml
2238               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2239                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2240              ProofEngine.proof := savedproof ;
2241              ProofEngine.goal := savedgoal ;
2242              refresh_sequent notebook
2243           | RefreshProofException e ->
2244              output_html outputhtml
2245               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2246                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2247              ProofEngine.proof := savedproof ;
2248              ProofEngine.goal := savedgoal ;
2249              refresh_sequent notebook ;
2250              refresh_proof output
2251           | e ->
2252              output_html outputhtml
2253               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2254              ProofEngine.proof := savedproof ;
2255              ProofEngine.goal := savedgoal ;
2256         end
2257    | [] ->
2258       output_html outputhtml
2259        ("<h1 color=\"red\">No term selected</h1>")
2260    | _ ->
2261       output_html outputhtml
2262        ("<h1 color=\"red\">Many terms selected</h1>")
2263 ;;
2264
2265
2266 let intros = call_tactic (ProofEngine.intros ~mk_fresh_name_callback);;
2267 let exact = call_tactic_with_input ProofEngine.exact;;
2268 let apply = call_tactic_with_input ProofEngine.apply;;
2269 let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl;;
2270 let elimtype = call_tactic_with_input ProofEngine.elim_type;;
2271 let whd = call_tactic_with_goal_inputs ProofEngine.whd;;
2272 let reduce = call_tactic_with_goal_inputs ProofEngine.reduce;;
2273 let simpl = call_tactic_with_goal_inputs ProofEngine.simpl;;
2274 let fold_whd = call_tactic_with_input ProofEngine.fold_whd;;
2275 let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce;;
2276 let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl;;
2277 let cut = call_tactic_with_input (ProofEngine.cut ~mk_fresh_name_callback);;
2278 let change = call_tactic_with_input_and_goal_input ProofEngine.change;;
2279 let letin = call_tactic_with_input (ProofEngine.letin ~mk_fresh_name_callback);;
2280 let ring = call_tactic ProofEngine.ring;;
2281 let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody;;
2282 let clear = call_tactic_with_hypothesis_input ProofEngine.clear;;
2283 let fourier = call_tactic ProofEngine.fourier;;
2284 let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl;;
2285 let rewritebacksimpl = call_tactic_with_input ProofEngine.rewrite_back_simpl;;
2286 let replace = call_tactic_with_input_and_goal_input ProofEngine.replace;;
2287 let reflexivity = call_tactic ProofEngine.reflexivity;;
2288 let symmetry = call_tactic ProofEngine.symmetry;;
2289 let transitivity = call_tactic_with_input ProofEngine.transitivity;;
2290 let exists = call_tactic ProofEngine.exists;;
2291 let split = call_tactic ProofEngine.split;;
2292 let left = call_tactic ProofEngine.left;;
2293 let right = call_tactic ProofEngine.right;;
2294 let assumption = call_tactic ProofEngine.assumption;;
2295 let generalize =
2296  call_tactic_with_goal_inputs (ProofEngine.generalize ~mk_fresh_name_callback);;
2297 let absurd = call_tactic_with_input ProofEngine.absurd;;
2298 let contradiction = call_tactic ProofEngine.contradiction;;
2299 let decompose =
2300  call_tactic_with_input
2301   (ProofEngine.decompose ~uris_choice_callback:decompose_uris_choice_callback);;
2302
2303 let whd_in_scratch scratch_window =
2304  call_tactic_with_goal_inputs_in_scratch ProofEngine.whd_in_scratch
2305   scratch_window
2306 ;;
2307 let reduce_in_scratch scratch_window =
2308  call_tactic_with_goal_inputs_in_scratch ProofEngine.reduce_in_scratch
2309   scratch_window
2310 ;;
2311 let simpl_in_scratch scratch_window =
2312  call_tactic_with_goal_inputs_in_scratch ProofEngine.simpl_in_scratch
2313   scratch_window
2314 ;;
2315
2316
2317
2318 (**********************)
2319 (*   END OF TACTICS   *)
2320 (**********************)
2321
2322
2323 let show () =
2324  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2325   try
2326    show_in_show_window_uri (input_or_locate_uri ~title:"Show")
2327   with
2328    e ->
2329     output_html outputhtml
2330      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2331 ;;
2332
2333 exception NotADefinition;;
2334
2335 let open_ () =
2336  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2337  let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
2338  let notebook = (rendering_window ())#notebook in
2339    try
2340     let uri = input_or_locate_uri ~title:"Open" in
2341      CicTypeChecker.typecheck uri ;
2342      let metasenv,bo,ty =
2343       match CicEnvironment.get_cooked_obj uri with
2344          Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
2345        | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
2346        | Cic.Constant _
2347        | Cic.Variable _
2348        | Cic.InductiveDefinition _ -> raise NotADefinition
2349      in
2350       ProofEngine.proof :=
2351        Some (uri, metasenv, bo, ty) ;
2352       ProofEngine.goal := None ;
2353       refresh_sequent notebook ;
2354       refresh_proof output
2355    with
2356       RefreshSequentException e ->
2357        output_html outputhtml
2358         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2359          "sequent: " ^ Printexc.to_string e ^ "</h1>")
2360     | RefreshProofException e ->
2361        output_html outputhtml
2362         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2363          "proof: " ^ Printexc.to_string e ^ "</h1>")
2364     | e ->
2365        output_html outputhtml
2366         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2367 ;;
2368
2369 let show_query_results results =
2370  let window =
2371   GWindow.window
2372    ~modal:false ~title:"Query results." ~border_width:2 () in
2373  let vbox = GPack.vbox ~packing:window#add () in
2374  let hbox =
2375   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2376  let lMessage =
2377   GMisc.label
2378    ~text:"Click on a URI to show that object"
2379    ~packing:hbox#add () in
2380  let scrolled_window =
2381   GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
2382    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2383  let clist = GList.clist ~columns:1 ~packing:scrolled_window#add () in
2384   ignore
2385    (List.map
2386      (function (uri,_) ->
2387        let n =
2388         clist#append [uri]
2389        in
2390         clist#set_row ~selectable:false n
2391      ) results
2392    ) ;
2393   clist#columns_autosize () ;
2394   ignore
2395    (clist#connect#select_row
2396      (fun ~row ~column ~event ->
2397        let (uristr,_) = List.nth results row in
2398         match
2399          Disambiguate.cic_textual_parser_uri_of_string
2400           (Disambiguate.wrong_xpointer_format_from_wrong_xpointer_format'
2401             uristr)
2402         with
2403            CicTextualParser0.ConUri uri
2404          | CicTextualParser0.VarUri uri
2405          | CicTextualParser0.IndTyUri (uri,_)
2406          | CicTextualParser0.IndConUri (uri,_,_) ->
2407             show_in_show_window_uri uri
2408      )
2409    ) ;
2410   window#show ()
2411 ;;
2412
2413 let refine_constraints (must_obj,must_rel,must_sort) =
2414  let chosen = ref false in
2415  let use_only = ref false in
2416  let window =
2417   GWindow.window
2418    ~modal:true ~title:"Constraints refinement."
2419    ~width:800 ~border_width:2 () in
2420  let vbox = GPack.vbox ~packing:window#add () in
2421  let hbox =
2422   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2423  let lMessage =
2424   GMisc.label
2425    ~text: "\"Only\" constraints can be enforced or not."
2426    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2427  let onlyb =
2428   GButton.toggle_button ~label:"Enforce \"only\" constraints"
2429    ~active:false ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2430  in
2431   ignore
2432    (onlyb#connect#toggled (function () -> use_only := onlyb#active)) ;
2433  (* Notebook for the constraints choice *)
2434  let notebook =
2435   GPack.notebook ~scrollable:true
2436    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2437  (* Rel constraints *)
2438  let label =
2439   GMisc.label
2440    ~text: "Constraints on Rels" () in
2441  let vbox' =
2442   GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
2443    () in
2444  let hbox =
2445   GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2446  let lMessage =
2447   GMisc.label
2448    ~text: "You can now specify the constraints on Rels."
2449    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2450  let expected_height = 25 * (List.length must_rel + 2) in
2451  let height = if expected_height > 400 then 400 else expected_height in
2452  let scrolled_window =
2453   GBin.scrolled_window ~border_width:10 ~height ~width:600
2454    ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
2455  let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
2456  let rel_constraints =
2457   List.map
2458    (function (position,depth) ->
2459      let hbox =
2460       GPack.hbox
2461        ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
2462      let lMessage =
2463       GMisc.label
2464        ~text:position
2465        ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2466      match depth with
2467         None -> position, ref None
2468       | Some depth' ->
2469          let mutable_ref = ref (Some depth') in
2470          let depthb =
2471           GButton.toggle_button
2472            ~label:("depth = " ^ string_of_int depth') ~active:true
2473            ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2474          in
2475           ignore
2476            (depthb#connect#toggled
2477              (function () ->
2478                let sel_depth = if depthb#active then Some depth' else None in
2479                 mutable_ref := sel_depth
2480             )) ;
2481           position, mutable_ref
2482    ) must_rel in
2483  (* Sort constraints *)
2484  let label =
2485   GMisc.label
2486    ~text: "Constraints on Sorts" () in
2487  let vbox' =
2488   GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
2489    () in
2490  let hbox =
2491   GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2492  let lMessage =
2493   GMisc.label
2494    ~text: "You can now specify the constraints on Sorts."
2495    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2496  let expected_height = 25 * (List.length must_sort + 2) in
2497  let height = if expected_height > 400 then 400 else expected_height in
2498  let scrolled_window =
2499   GBin.scrolled_window ~border_width:10 ~height ~width:600
2500    ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
2501  let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
2502  let sort_constraints =
2503   List.map
2504    (function (position,depth,sort) ->
2505      let hbox =
2506       GPack.hbox
2507        ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
2508      let lMessage =
2509       GMisc.label
2510        ~text:(sort ^ " " ^ position)
2511        ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2512      match depth with
2513         None -> position, ref None, sort
2514       | Some depth' ->
2515          let mutable_ref = ref (Some depth') in
2516          let depthb =
2517           GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
2518            ~active:true
2519            ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2520          in
2521           ignore
2522            (depthb#connect#toggled
2523              (function () ->
2524                let sel_depth = if depthb#active then Some depth' else None in
2525                 mutable_ref := sel_depth
2526             )) ;
2527           position, mutable_ref, sort
2528    ) must_sort in
2529  (* Obj constraints *)
2530  let label =
2531   GMisc.label
2532    ~text: "Constraints on constants" () in
2533  let vbox' =
2534   GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
2535    () in
2536  let hbox =
2537   GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2538  let lMessage =
2539   GMisc.label
2540    ~text: "You can now specify the constraints on constants."
2541    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2542  let expected_height = 25 * (List.length must_obj + 2) in
2543  let height = if expected_height > 400 then 400 else expected_height in
2544  let scrolled_window =
2545   GBin.scrolled_window ~border_width:10 ~height ~width:600
2546    ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
2547  let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
2548  let obj_constraints =
2549   List.map
2550    (function (uri,position,depth) ->
2551      let hbox =
2552       GPack.hbox
2553        ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
2554      let lMessage =
2555       GMisc.label
2556        ~text:(uri ^ " " ^ position)
2557        ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2558      match depth with
2559         None -> uri, position, ref None
2560       | Some depth' ->
2561          let mutable_ref = ref (Some depth') in
2562          let depthb =
2563           GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
2564            ~active:true
2565            ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2566          in
2567           ignore
2568            (depthb#connect#toggled
2569              (function () ->
2570                let sel_depth = if depthb#active then Some depth' else None in
2571                 mutable_ref := sel_depth
2572             )) ;
2573           uri, position, mutable_ref
2574    ) must_obj in
2575  (* Confirm/abort buttons *)
2576  let hbox =
2577   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2578  let okb =
2579   GButton.button ~label:"Ok"
2580    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2581  let cancelb =
2582   GButton.button ~label:"Abort"
2583    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2584  in
2585   ignore (window#connect#destroy GMain.Main.quit) ;
2586   ignore (cancelb#connect#clicked window#destroy) ;
2587   ignore
2588    (okb#connect#clicked (function () -> chosen := true ; window#destroy ()));
2589   window#set_position `CENTER ;
2590   window#show () ;
2591   GMain.Main.main () ;
2592   if !chosen then
2593    let chosen_must_rel =
2594     List.map
2595      (function (position,ref_depth) -> position,!ref_depth) rel_constraints in
2596    let chosen_must_sort =
2597     List.map
2598      (function (position,ref_depth,sort) -> position,!ref_depth,sort)
2599      sort_constraints
2600    in
2601    let chosen_must_obj =
2602     List.map
2603      (function (uri,position,ref_depth) -> uri,position,!ref_depth)
2604      obj_constraints
2605    in
2606     (chosen_must_obj,chosen_must_rel,chosen_must_sort),
2607      (if !use_only then
2608 (*CSC: ???????????????????????? I assume that must and only are the same... *)
2609        Some chosen_must_obj,Some chosen_must_rel,Some chosen_must_sort
2610       else
2611        None,None,None
2612      )
2613   else
2614    raise NoChoice
2615 ;;
2616
2617 let completeSearchPattern () =
2618  let inputt = ((rendering_window ())#inputt : term_editor) in
2619  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2620   try
2621    let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
2622    let must = MQueryLevels2.get_constraints expr in
2623    let must',only = refine_constraints must in
2624    let results = MQueryGenerator.searchPattern must' only in
2625     show_query_results results
2626   with
2627    e ->
2628     output_html outputhtml
2629      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2630 ;;
2631
2632 let insertQuery () =
2633  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2634   try
2635    let chosen = ref None in
2636    let window =
2637     GWindow.window
2638      ~modal:true ~title:"Insert Query (Experts Only)" ~border_width:2 () in
2639    let vbox = GPack.vbox ~packing:window#add () in
2640    let label =
2641     GMisc.label ~text:"Insert Query. For Experts Only."
2642      ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2643    let scrolled_window =
2644     GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
2645      ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2646    let input = GEdit.text ~editable:true
2647     ~packing:scrolled_window#add () in
2648    let hbox =
2649     GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2650    let okb =
2651     GButton.button ~label:"Ok"
2652      ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2653    let loadb =
2654     GButton.button ~label:"Load from file..."
2655      ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2656    let cancelb =
2657     GButton.button ~label:"Abort"
2658      ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2659    ignore (window#connect#destroy GMain.Main.quit) ;
2660    ignore (cancelb#connect#clicked window#destroy) ;
2661    ignore
2662     (okb#connect#clicked
2663       (function () ->
2664         chosen := Some (input#get_chars 0 input#length) ; window#destroy ())) ;
2665    ignore
2666     (loadb#connect#clicked
2667       (function () ->
2668         match
2669          GToolbox.select_file ~title:"Select Query File" ()
2670         with
2671            None -> ()
2672          | Some filename ->
2673             let inch = open_in filename in
2674              let rec read_file () =
2675               try
2676                let line = input_line inch in
2677                 line ^ "\n" ^ read_file ()
2678               with
2679                End_of_file -> ""
2680              in
2681               let text = read_file () in
2682                input#delete_text 0 input#length ;
2683                ignore (input#insert_text text ~pos:0))) ;
2684    window#set_position `CENTER ;
2685    window#show () ;
2686    GMain.Main.main () ;
2687    match !chosen with
2688       None -> ()
2689     | Some q ->
2690        let results =
2691         Mqint.execute (MQueryUtil.query_of_text (Lexing.from_string q))
2692        in
2693         show_query_results results
2694   with
2695    e ->
2696     output_html outputhtml
2697      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2698 ;;
2699
2700 let choose_must list_of_must only =
2701  let chosen = ref None in
2702  let user_constraints = ref [] in
2703  let window =
2704   GWindow.window
2705    ~modal:true ~title:"Query refinement." ~border_width:2 () in
2706  let vbox = GPack.vbox ~packing:window#add () in
2707  let hbox =
2708   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2709  let lMessage =
2710   GMisc.label
2711    ~text:
2712     ("You can now specify the genericity of the query. " ^
2713      "The more generic the slower.")
2714    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2715  let hbox =
2716   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2717  let lMessage =
2718   GMisc.label
2719    ~text:
2720     "Suggestion: start with faster queries before moving to more generic ones."
2721    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2722  let notebook =
2723   GPack.notebook ~scrollable:true
2724    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2725  let _ =
2726   let page = ref 0 in
2727   let last = List.length list_of_must in
2728   List.map
2729    (function must ->
2730      incr page ;
2731      let label =
2732       GMisc.label ~text:
2733        (if !page = 1 then "More generic" else
2734          if !page = last then "More precise" else "          ") () in
2735      let expected_height = 25 * (List.length must + 2) in
2736      let height = if expected_height > 400 then 400 else expected_height in
2737      let scrolled_window =
2738       GBin.scrolled_window ~border_width:10 ~height ~width:600
2739        ~packing:(notebook#append_page ~tab_label:label#coerce) () in
2740      let clist =
2741         GList.clist ~columns:2 ~packing:scrolled_window#add
2742          ~titles:["URI" ; "Position"] ()
2743      in
2744       ignore
2745        (List.map
2746          (function (uri,position) ->
2747            let n =
2748             clist#append
2749              [uri; if position then "MainConclusion" else "Conclusion"]
2750            in
2751             clist#set_row ~selectable:false n
2752          ) must
2753        ) ;
2754       clist#columns_autosize ()
2755    ) list_of_must in
2756  let _ =
2757   let label = GMisc.label ~text:"User provided" () in
2758   let vbox =
2759    GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) () in
2760   let hbox =
2761    GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2762   let lMessage =
2763    GMisc.label
2764    ~text:"Select the constraints that must be satisfied and press OK."
2765    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2766   let expected_height = 25 * (List.length only + 2) in
2767   let height = if expected_height > 400 then 400 else expected_height in
2768   let scrolled_window =
2769    GBin.scrolled_window ~border_width:10 ~height ~width:600
2770     ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2771   let clist =
2772    GList.clist ~columns:2 ~packing:scrolled_window#add
2773     ~selection_mode:`EXTENDED
2774     ~titles:["URI" ; "Position"] ()
2775   in
2776    ignore
2777     (List.map
2778       (function (uri,position) ->
2779         let n =
2780          clist#append
2781           [uri; if position then "MainConclusion" else "Conclusion"]
2782         in
2783          clist#set_row ~selectable:true n
2784       ) only
2785     ) ;
2786    clist#columns_autosize () ;
2787    ignore
2788     (clist#connect#select_row
2789       (fun ~row ~column ~event ->
2790         user_constraints := (List.nth only row)::!user_constraints)) ;
2791    ignore
2792     (clist#connect#unselect_row
2793       (fun ~row ~column ~event ->
2794         user_constraints :=
2795          List.filter
2796           (function uri -> uri != (List.nth only row)) !user_constraints)) ;
2797  in
2798  let hbox =
2799   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2800  let okb =
2801   GButton.button ~label:"Ok"
2802    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2803  let cancelb =
2804   GButton.button ~label:"Abort"
2805    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2806  (* actions *)
2807  ignore (window#connect#destroy GMain.Main.quit) ;
2808  ignore (cancelb#connect#clicked window#destroy) ;
2809  ignore
2810   (okb#connect#clicked
2811     (function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
2812  window#set_position `CENTER ;
2813  window#show () ;
2814  GMain.Main.main () ;
2815  match !chosen with
2816     None -> raise NoChoice
2817   | Some n ->
2818      if n = List.length list_of_must then
2819       (* user provided constraints *)
2820       !user_constraints
2821      else
2822       List.nth list_of_must n
2823 ;;
2824
2825 let searchPattern () =
2826  let inputt = ((rendering_window ())#inputt : term_editor) in
2827  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2828   try
2829     let metasenv =
2830      match !ProofEngine.proof with
2831         None -> assert false
2832       | Some (_,metasenv,_,_) -> metasenv
2833     in
2834      match !ProofEngine.goal with
2835         None -> ()
2836       | Some metano ->
2837          let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
2838           let list_of_must,only = MQueryLevels.out_restr metasenv ey ty in
2839           let must = choose_must list_of_must only in
2840           let torigth_restriction (u,b) =
2841            let p =
2842             if b then
2843              "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion"
2844             else
2845              "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"
2846            in
2847             (u,p,None)
2848           in
2849           let rigth_must = List.map torigth_restriction must in
2850           let rigth_only = Some (List.map torigth_restriction only) in
2851           let result =
2852            MQueryGenerator.searchPattern
2853             (rigth_must,[],[]) (rigth_only,None,None) in
2854           let uris =
2855            List.map
2856             (function uri,_ ->
2857               Disambiguate.wrong_xpointer_format_from_wrong_xpointer_format' uri
2858             ) result in
2859           let html =
2860            " <h1>Backward Query: </h1>" ^
2861            " <pre>" ^ get_last_query result ^ "</pre>"
2862           in
2863            output_html outputhtml html ;
2864            let uris',exc =
2865             let rec filter_out =
2866              function
2867                 [] -> [],""
2868               | uri::tl ->
2869                  let tl',exc = filter_out tl in
2870                   try
2871                    if
2872                     ProofEngine.can_apply
2873                      (term_of_cic_textual_parser_uri
2874                       (Disambiguate.cic_textual_parser_uri_of_string uri))
2875                    then
2876                     uri::tl',exc
2877                    else
2878                     tl',exc
2879                   with
2880                    e ->
2881                     let exc' =
2882                      "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
2883                       uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
2884                     in
2885                      tl',exc'
2886             in
2887              filter_out uris
2888            in
2889             let html' =
2890              " <h1>Objects that can actually be applied: </h1> " ^
2891              String.concat "<br>" uris' ^ exc ^
2892              " <h1>Number of false matches: " ^
2893               string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
2894              " <h1>Number of good matches: " ^
2895               string_of_int (List.length uris') ^ "</h1>"
2896             in
2897              output_html outputhtml html' ;
2898              let uri' =
2899               user_uri_choice ~title:"Ambiguous input."
2900               ~msg:
2901                 "Many lemmas can be successfully applied. Please, choose one:"
2902                uris'
2903              in
2904               inputt#set_term uri' ;
2905               apply ()
2906   with
2907    e ->
2908     output_html outputhtml
2909      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2910 ;;
2911
2912 let choose_selection mmlwidget (element : Gdome.element option) =
2913  let module G = Gdome in
2914   let rec aux element =
2915    if element#hasAttributeNS
2916        ~namespaceURI:helmns
2917        ~localName:(G.domString "xref")
2918    then
2919      mmlwidget#set_selection (Some element)
2920    else
2921     try
2922       match element#get_parentNode with
2923          None -> assert false
2924        (*CSC: OCAML DIVERGES!
2925        | Some p -> aux (new G.element_of_node p)
2926        *)
2927        | Some p -> aux (new Gdome.element_of_node p)
2928     with
2929        GdomeInit.DOMCastException _ ->
2930         prerr_endline
2931          "******* trying to select above the document root ********"
2932   in
2933    match element with
2934      Some x -> aux x
2935    | None   -> mmlwidget#set_selection None
2936 ;;
2937
2938 (* STUFF TO BUILD THE GTK INTERFACE *)
2939
2940 (* Stuff for the widget settings *)
2941
2942 let export_to_postscript (output : GMathViewAux.single_selection_math_view) =
2943  let lastdir = ref (Unix.getcwd ()) in
2944   function () ->
2945    match
2946     GToolbox.select_file ~title:"Export to PostScript"
2947      ~dir:lastdir ~filename:"screenshot.ps" ()
2948    with
2949       None -> ()
2950     | Some filename ->
2951        output#export_to_postscript ~filename:filename ();
2952 ;;
2953
2954 let activate_t1 (output : GMathViewAux.single_selection_math_view) button_set_anti_aliasing
2955  button_set_transparency export_to_postscript_menu_item
2956  button_t1 ()
2957 =
2958  let is_set = button_t1#active in
2959   output#set_font_manager_type
2960    (if is_set then `font_manager_t1 else `font_manager_gtk) ;
2961   if is_set then
2962    begin
2963     button_set_anti_aliasing#misc#set_sensitive true ;
2964     button_set_transparency#misc#set_sensitive true ;
2965     export_to_postscript_menu_item#misc#set_sensitive true ;
2966    end
2967   else
2968    begin
2969     button_set_anti_aliasing#misc#set_sensitive false ;
2970     button_set_transparency#misc#set_sensitive false ;
2971     export_to_postscript_menu_item#misc#set_sensitive false ;
2972    end
2973 ;;
2974
2975 let set_anti_aliasing output button_set_anti_aliasing () =
2976  output#set_anti_aliasing button_set_anti_aliasing#active
2977 ;;
2978
2979 let set_transparency output button_set_transparency () =
2980  output#set_transparency button_set_transparency#active
2981 ;;
2982
2983 let changefont output font_size_spinb () =
2984  output#set_font_size font_size_spinb#value_as_int
2985 ;;
2986
2987 let set_log_verbosity output log_verbosity_spinb () =
2988  output#set_log_verbosity log_verbosity_spinb#value_as_int
2989 ;;
2990
2991 class settings_window (output : GMathViewAux.single_selection_math_view) sw
2992  export_to_postscript_menu_item selection_changed_callback
2993 =
2994  let settings_window = GWindow.window ~title:"GtkMathView settings" () in
2995  let vbox =
2996   GPack.vbox ~packing:settings_window#add () in
2997  let table =
2998   GPack.table
2999    ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
3000    ~border_width:5 ~packing:vbox#add () in
3001  let button_t1 =
3002   GButton.toggle_button ~label:"activate t1 fonts"
3003    ~packing:(table#attach ~left:0 ~top:0) () in
3004  let button_set_anti_aliasing =
3005   GButton.toggle_button ~label:"set_anti_aliasing"
3006    ~packing:(table#attach ~left:0 ~top:1) () in
3007  let button_set_transparency =
3008   GButton.toggle_button ~label:"set_transparency"
3009    ~packing:(table#attach ~left:2 ~top:1) () in
3010  let table =
3011   GPack.table
3012    ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
3013    ~border_width:5 ~packing:vbox#add () in
3014  let font_size_label =
3015   GMisc.label ~text:"font size:"
3016    ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
3017  let font_size_spinb =
3018   let sadj =
3019    GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
3020   in
3021    GEdit.spin_button
3022     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
3023  let log_verbosity_label =
3024   GMisc.label ~text:"log verbosity:"
3025    ~packing:(table#attach ~left:0 ~top:1) () in
3026  let log_verbosity_spinb =
3027   let sadj =
3028    GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
3029   in
3030    GEdit.spin_button
3031     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
3032  let hbox =
3033   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
3034  let closeb =
3035   GButton.button ~label:"Close"
3036    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
3037 object(self)
3038  method show = settings_window#show
3039  initializer
3040   button_set_anti_aliasing#misc#set_sensitive false ;
3041   button_set_transparency#misc#set_sensitive false ;
3042   (* Signals connection *)
3043   ignore(button_t1#connect#clicked
3044    (activate_t1 output button_set_anti_aliasing
3045     button_set_transparency export_to_postscript_menu_item button_t1)) ;
3046   ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
3047   ignore(button_set_anti_aliasing#connect#toggled
3048    (set_anti_aliasing output button_set_anti_aliasing));
3049   ignore(button_set_transparency#connect#toggled
3050    (set_transparency output button_set_transparency)) ;
3051   ignore(log_verbosity_spinb#connect#changed
3052    (set_log_verbosity output log_verbosity_spinb)) ;
3053   ignore(closeb#connect#clicked settings_window#misc#hide)
3054 end;;
3055
3056 (* Scratch window *)
3057
3058 class scratch_window =
3059  let window =
3060   GWindow.window ~title:"MathML viewer" ~border_width:2 () in
3061  let vbox =
3062   GPack.vbox ~packing:window#add () in
3063  let hbox =
3064   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
3065  let whdb =
3066   GButton.button ~label:"Whd"
3067    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
3068  let reduceb =
3069   GButton.button ~label:"Reduce"
3070    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
3071  let simplb =
3072   GButton.button ~label:"Simpl"
3073    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
3074  let scrolled_window =
3075   GBin.scrolled_window ~border_width:10
3076    ~packing:(vbox#pack ~expand:true ~padding:5) () in
3077  let mmlwidget =
3078   GMathViewAux.multi_selection_math_view
3079    ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
3080 object(self)
3081  method mmlwidget = mmlwidget
3082  method show () = window#misc#hide () ; window#show ()
3083  initializer
3084   ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
3085   ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
3086   ignore(whdb#connect#clicked (whd_in_scratch self)) ;
3087   ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
3088   ignore(simplb#connect#clicked (simpl_in_scratch self))
3089 end;;
3090
3091 let open_contextual_menu_for_selected_terms mmlwidget infos =
3092  let button = GdkEvent.Button.button infos in
3093  let terms_selected = List.length mmlwidget#get_selections > 0 in
3094   if button = 3 then
3095    begin
3096     let time = GdkEvent.Button.time infos in
3097     let menu = GMenu.menu () in
3098     let f = new GMenu.factory menu in
3099     let whd_menu_item =
3100      f#add_item "Whd" ~key:GdkKeysyms._W ~callback:whd in
3101     let reduce_menu_item =
3102      f#add_item "Reduce" ~key:GdkKeysyms._R ~callback:reduce in
3103     let simpl_menu_item =
3104      f#add_item "Simpl" ~key:GdkKeysyms._S ~callback:simpl in
3105     let _ = f#add_separator () in
3106     let generalize_menu_item =
3107      f#add_item "Generalize" ~key:GdkKeysyms._G ~callback:generalize
3108     in
3109      whd_menu_item#misc#set_sensitive terms_selected ;
3110      reduce_menu_item#misc#set_sensitive terms_selected ;
3111      simpl_menu_item#misc#set_sensitive terms_selected ;
3112      generalize_menu_item#misc#set_sensitive terms_selected ;
3113      menu#popup ~button ~time
3114    end ;
3115   true
3116 ;;
3117
3118 class page () =
3119  let vbox1 = GPack.vbox () in
3120 object(self)
3121  val mutable proofw_ref = None
3122  val mutable compute_ref = None
3123  method proofw =
3124   Lazy.force self#compute ;
3125   match proofw_ref with
3126      None -> assert false
3127    | Some proofw -> proofw
3128  method content = vbox1
3129  method compute =
3130   match compute_ref with
3131      None -> assert false
3132    | Some compute -> compute
3133  initializer
3134   compute_ref <-
3135    Some (lazy (
3136    let scrolled_window1 =
3137     GBin.scrolled_window ~border_width:10
3138      ~packing:(vbox1#pack ~expand:true ~padding:5) () in
3139    let proofw =
3140     GMathViewAux.multi_selection_math_view ~width:400 ~height:275
3141      ~packing:(scrolled_window1#add) () in
3142    let _ = proofw_ref <- Some proofw in
3143    let hbox3 =
3144     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3145    let exactb =
3146     GButton.button ~label:"Exact"
3147      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3148    let introsb =
3149     GButton.button ~label:"Intros"
3150      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3151    let applyb =
3152     GButton.button ~label:"Apply"
3153      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3154    let elimintrossimplb =
3155     GButton.button ~label:"ElimIntrosSimpl"
3156      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3157    let elimtypeb =
3158     GButton.button ~label:"ElimType"
3159      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3160 (* Zack: spostare in una toolbar
3161    let whdb =
3162     GButton.button ~label:"Whd"
3163      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3164    let reduceb =
3165     GButton.button ~label:"Reduce"
3166      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3167    let simplb =
3168     GButton.button ~label:"Simpl"
3169      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3170 *)
3171    let hbox4 =
3172     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3173    let foldwhdb =
3174     GButton.button ~label:"Fold_whd"
3175      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3176    let foldreduceb =
3177     GButton.button ~label:"Fold_reduce"
3178      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3179    let foldsimplb =
3180     GButton.button ~label:"Fold_simpl"
3181      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3182    let cutb =
3183     GButton.button ~label:"Cut"
3184      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3185    let changeb =
3186     GButton.button ~label:"Change"
3187      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3188    let letinb =
3189     GButton.button ~label:"Let ... In"
3190      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3191    let ringb =
3192     GButton.button ~label:"Ring"
3193      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3194    let hbox5 =
3195     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3196    let clearbodyb =
3197     GButton.button ~label:"ClearBody"
3198      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3199    let clearb =
3200     GButton.button ~label:"Clear"
3201      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3202    let fourierb =
3203     GButton.button ~label:"Fourier"
3204      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3205    let rewritesimplb =
3206     GButton.button ~label:"RewriteSimpl ->"
3207      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3208    let rewritebacksimplb =
3209     GButton.button ~label:"RewriteSimpl <-"
3210      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3211    let replaceb =
3212     GButton.button ~label:"Replace"
3213      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3214    let hbox6 =
3215     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3216    let reflexivityb =
3217     GButton.button ~label:"Reflexivity"
3218      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3219    let symmetryb =
3220     GButton.button ~label:"Symmetry"
3221      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3222    let transitivityb =
3223     GButton.button ~label:"Transitivity"
3224      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3225    let existsb =
3226     GButton.button ~label:"Exists"
3227      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3228    let splitb =
3229     GButton.button ~label:"Split"
3230      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3231    let leftb =
3232     GButton.button ~label:"Left"
3233      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3234    let rightb =
3235     GButton.button ~label:"Right"
3236      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3237    let assumptionb =
3238     GButton.button ~label:"Assumption"
3239      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3240    let hbox7 =
3241     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3242 (* Zack: spostare in una toolbar
3243    let generalizeb =
3244     GButton.button ~label:"Generalize"
3245      ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3246 *)
3247    let absurdb =
3248     GButton.button ~label:"Absurd"
3249      ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3250    let contradictionb =
3251     GButton.button ~label:"Contradiction"
3252      ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3253    let searchpatternb =
3254     GButton.button ~label:"SearchPattern_Apply"
3255      ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3256    let decomposeb =
3257     GButton.button ~label:"Decompose"
3258      ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3259
3260    ignore(exactb#connect#clicked exact) ;
3261    ignore(applyb#connect#clicked apply) ;
3262    ignore(elimintrossimplb#connect#clicked elimintrossimpl) ;
3263    ignore(elimtypeb#connect#clicked elimtype) ;
3264 (* Zack: spostare in una toolbar
3265    ignore(whdb#connect#clicked whd) ;
3266    ignore(reduceb#connect#clicked reduce) ;
3267    ignore(simplb#connect#clicked simpl) ;
3268 *)
3269    ignore(foldwhdb#connect#clicked fold_whd) ;
3270    ignore(foldreduceb#connect#clicked fold_reduce) ;
3271    ignore(foldsimplb#connect#clicked fold_simpl) ;
3272    ignore(cutb#connect#clicked cut) ;
3273    ignore(changeb#connect#clicked change) ;
3274    ignore(letinb#connect#clicked letin) ;
3275    ignore(ringb#connect#clicked ring) ;
3276    ignore(clearbodyb#connect#clicked clearbody) ;
3277    ignore(clearb#connect#clicked clear) ;
3278    ignore(fourierb#connect#clicked fourier) ;
3279    ignore(rewritesimplb#connect#clicked rewritesimpl) ;
3280    ignore(rewritebacksimplb#connect#clicked rewritebacksimpl) ;
3281    ignore(replaceb#connect#clicked replace) ;
3282    ignore(reflexivityb#connect#clicked reflexivity) ;
3283    ignore(symmetryb#connect#clicked symmetry) ;
3284    ignore(transitivityb#connect#clicked transitivity) ;
3285    ignore(existsb#connect#clicked exists) ;
3286    ignore(splitb#connect#clicked split) ;
3287    ignore(leftb#connect#clicked left) ;
3288    ignore(rightb#connect#clicked right) ;
3289    ignore(assumptionb#connect#clicked assumption) ;
3290 (* Zack: spostare in una toolbar
3291    ignore(generalizeb#connect#clicked generalize) ;
3292 *)
3293    ignore(absurdb#connect#clicked absurd) ;
3294    ignore(contradictionb#connect#clicked contradiction) ;
3295    ignore(introsb#connect#clicked intros) ;
3296    ignore(searchpatternb#connect#clicked searchPattern) ;
3297    ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
3298    ignore
3299      ((new GObj.event_ops proofw#as_widget)#connect#button_press
3300         (open_contextual_menu_for_selected_terms proofw)) ;
3301    ignore(decomposeb#connect#clicked decompose) ;
3302   ))
3303 end
3304 ;;
3305
3306 class empty_page =
3307  let vbox1 = GPack.vbox () in
3308  let scrolled_window1 =
3309   GBin.scrolled_window ~border_width:10
3310    ~packing:(vbox1#pack ~expand:true ~padding:5) () in
3311  let proofw =
3312   GMathViewAux.single_selection_math_view ~width:400 ~height:275
3313    ~packing:(scrolled_window1#add) () in
3314 object(self)
3315  method proofw = (assert false : GMathViewAux.single_selection_math_view)
3316  method content = vbox1
3317  method compute = (assert false : unit)
3318 end
3319 ;;
3320
3321 let empty_page = new empty_page;;
3322
3323 class notebook =
3324 object(self)
3325  val notebook = GPack.notebook ()
3326  val pages = ref []
3327  val mutable skip_switch_page_event = false
3328  val mutable empty = true
3329  method notebook = notebook
3330  method add_page n =
3331   let new_page = new page () in
3332    empty <- false ;
3333    pages := !pages @ [n,lazy (setgoal n),new_page] ;
3334    notebook#append_page
3335     ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce)
3336     new_page#content#coerce
3337  method remove_all_pages ~skip_switch_page_event:skip =
3338   if empty then
3339    notebook#remove_page 0 (* let's remove the empty page *)
3340   else
3341    List.iter (function _ -> notebook#remove_page 0) !pages ;
3342   pages := [] ;
3343   skip_switch_page_event <- skip
3344  method set_current_page ~may_skip_switch_page_event n =
3345   let (_,_,page) = List.find (function (m,_,_) -> m=n) !pages in
3346    let new_page = notebook#page_num page#content#coerce in
3347     if may_skip_switch_page_event && new_page <> notebook#current_page then
3348      skip_switch_page_event <- true ;
3349     notebook#goto_page new_page
3350  method set_empty_page =
3351   empty <- true ;
3352   pages := [] ;
3353   notebook#append_page
3354    ~tab_label:((GMisc.label ~text:"No proof in progress" ())#coerce)
3355    empty_page#content#coerce
3356  method proofw =
3357   let (_,_,page) = List.nth !pages notebook#current_page in
3358    page#proofw
3359  initializer
3360   ignore
3361    (notebook#connect#switch_page
3362     (function i ->
3363       let skip = skip_switch_page_event in
3364        skip_switch_page_event <- false ;
3365        if not skip then
3366         try
3367          let (metano,setgoal,page) = List.nth !pages i in
3368           ProofEngine.goal := Some metano ;
3369           Lazy.force (page#compute) ;
3370           Lazy.force setgoal
3371         with _ -> ()
3372     ))
3373 end
3374 ;;
3375
3376 (* Main window *)
3377
3378 class rendering_window output (notebook : notebook) =
3379  let scratch_window = new scratch_window in
3380  let window =
3381   GWindow.window ~title:"MathML viewer" ~border_width:0
3382    ~allow_shrink:false () in
3383  let vbox_for_menu = GPack.vbox ~packing:window#add () in
3384  (* menus *)
3385  let handle_box = GBin.handle_box ~border_width:2
3386   ~packing:(vbox_for_menu#pack ~padding:0) () in
3387  let menubar = GMenu.menu_bar ~packing:handle_box#add () in
3388  let factory0 = new GMenu.factory menubar in
3389  let accel_group = factory0#accel_group in
3390  (* file menu *)
3391  let file_menu = factory0#add_submenu "File" in
3392  let factory1 = new GMenu.factory file_menu ~accel_group in
3393  let export_to_postscript_menu_item =
3394   begin
3395    let _ =
3396     factory1#add_item "New Block of (Co)Inductive Definitions..."
3397      ~key:GdkKeysyms._B ~callback:new_inductive
3398    in
3399    let _ =
3400     factory1#add_item "New Proof or Definition..." ~key:GdkKeysyms._N
3401      ~callback:new_proof
3402    in
3403    let reopen_menu_item =
3404     factory1#add_item "Reopen a Finished Proof..." ~key:GdkKeysyms._R
3405      ~callback:open_
3406    in
3407    let qed_menu_item =
3408     factory1#add_item "Qed" ~key:GdkKeysyms._E ~callback:qed in
3409    ignore (factory1#add_separator ()) ;
3410    ignore
3411     (factory1#add_item "Load Unfinished Proof..." ~key:GdkKeysyms._L
3412       ~callback:load) ;
3413    let save_menu_item =
3414     factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S ~callback:save
3415    in
3416    ignore
3417     (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b);
3418    ignore (!save_set_sensitive false);
3419    ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b);
3420    ignore (!qed_set_sensitive false);
3421    ignore (factory1#add_separator ()) ;
3422    let export_to_postscript_menu_item =
3423     factory1#add_item "Export to PostScript..."
3424      ~callback:(export_to_postscript output) in
3425    ignore (factory1#add_separator ()) ;
3426    ignore
3427     (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) ;
3428    export_to_postscript_menu_item
3429   end in
3430  (* edit menu *)
3431  let edit_menu = factory0#add_submenu "Edit Current Proof" in
3432  let factory2 = new GMenu.factory edit_menu ~accel_group in
3433  let focus_and_proveit_set_sensitive = ref (function _ -> assert false) in
3434  let proveit_menu_item =
3435   factory2#add_item "Prove It" ~key:GdkKeysyms._I
3436    ~callback:(function () -> proveit ();!focus_and_proveit_set_sensitive false)
3437  in
3438  let focus_menu_item =
3439   factory2#add_item "Focus" ~key:GdkKeysyms._F
3440    ~callback:(function () -> focus () ; !focus_and_proveit_set_sensitive false)
3441  in
3442  let _ =
3443   focus_and_proveit_set_sensitive :=
3444    function b ->
3445     proveit_menu_item#misc#set_sensitive b ;
3446     focus_menu_item#misc#set_sensitive b
3447  in
3448  let _ = !focus_and_proveit_set_sensitive false in
3449  (* edit term menu *)
3450  let edit_term_menu = factory0#add_submenu "Edit Term" in
3451  let factory5 = new GMenu.factory edit_term_menu ~accel_group in
3452  let check_menu_item =
3453   factory5#add_item "Check Term" ~key:GdkKeysyms._C
3454    ~callback:(check scratch_window) in
3455  let _ = check_menu_item#misc#set_sensitive false in
3456  (* search menu *)
3457  let settings_menu = factory0#add_submenu "Search" in
3458  let factory4 = new GMenu.factory settings_menu ~accel_group in
3459  let _ =
3460   factory4#add_item "Locate..." ~key:GdkKeysyms._T
3461    ~callback:locate in
3462  let searchPattern_menu_item =
3463   factory4#add_item "SearchPattern..." ~key:GdkKeysyms._D
3464    ~callback:completeSearchPattern in
3465  let _ = searchPattern_menu_item#misc#set_sensitive false in
3466  let show_menu_item =
3467   factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show
3468  in
3469  let insert_query_item =
3470   factory4#add_item "Insert Query (Experts Only)..." ~key:GdkKeysyms._U
3471    ~callback:insertQuery in
3472  (* settings menu *)
3473  let settings_menu = factory0#add_submenu "Settings" in
3474  let factory3 = new GMenu.factory settings_menu ~accel_group in
3475  let _ =
3476   factory3#add_item "Edit Aliases" ~key:GdkKeysyms._A
3477    ~callback:edit_aliases in
3478  let _ = factory3#add_separator () in
3479  let _ =
3480   factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P
3481    ~callback:(function _ -> (settings_window ())#show ()) in
3482  (* accel group *)
3483  let _ = window#add_accel_group accel_group in
3484  (* end of menus *)
3485  let hbox0 =
3486   GPack.hbox
3487    ~packing:(vbox_for_menu#pack ~expand:true ~fill:true ~padding:5) () in
3488  let vbox =
3489   GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
3490  let scrolled_window0 =
3491   GBin.scrolled_window ~border_width:10
3492    ~packing:(vbox#pack ~expand:true ~padding:5) () in
3493  let _ = scrolled_window0#add output#coerce in
3494  let frame =
3495   GBin.frame ~label:"Insert Term"
3496    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
3497  let scrolled_window1 =
3498   GBin.scrolled_window ~border_width:5
3499    ~packing:frame#add () in
3500  let inputt =
3501   new term_editor ~width:400 ~height:100 ~packing:scrolled_window1#add ()
3502    ~isnotempty_callback:
3503     (function b ->
3504       check_menu_item#misc#set_sensitive b ;
3505       searchPattern_menu_item#misc#set_sensitive b) in
3506  let vboxl =
3507   GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
3508  let _ =
3509   vboxl#pack ~expand:true ~fill:true ~padding:5 notebook#notebook#coerce in
3510  let frame =
3511   GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
3512  in
3513  let outputhtml =
3514   GHtml.xmhtml
3515    ~source:"<html><body bgColor=\"white\"></body></html>"
3516    ~width:400 ~height: 100
3517    ~border_width:20
3518    ~packing:frame#add
3519    ~show:true () in
3520 object
3521  method outputhtml = outputhtml
3522  method inputt = inputt
3523  method output = (output : GMathViewAux.single_selection_math_view)
3524  method notebook = notebook
3525  method show = window#show
3526  initializer
3527   notebook#set_empty_page ;
3528   export_to_postscript_menu_item#misc#set_sensitive false ;
3529   check_term := (check_term_in_scratch scratch_window) ;
3530
3531   (* signal handlers here *)
3532   ignore(output#connect#selection_changed
3533    (function elem ->
3534      choose_selection output elem ;
3535      !focus_and_proveit_set_sensitive true
3536    )) ;
3537   ignore (output#connect#click (show_in_show_window_callback output)) ;
3538   let settings_window = new settings_window output scrolled_window0
3539    export_to_postscript_menu_item (choose_selection output) in
3540   set_settings_window settings_window ;
3541   set_outputhtml outputhtml ;
3542   ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
3543   Logger.log_callback :=
3544    (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
3545 end;;
3546
3547 (* MAIN *)
3548
3549 let initialize_everything () =
3550  let module U = Unix in
3551   let output = GMathViewAux.single_selection_math_view ~width:350 ~height:280 () in
3552   let notebook = new notebook in
3553    let rendering_window' = new rendering_window output notebook in
3554     set_rendering_window rendering_window' ;
3555     mml_of_cic_term_ref := mml_of_cic_term ;
3556     rendering_window'#show () ;
3557     GMain.Main.main ()
3558 ;;
3559
3560 let _ =
3561  if !usedb then
3562   begin
3563    Mqint.set_database Mqint.postgres_db ;
3564    Mqint.init postgresqlconnectionstring ;
3565   end ;
3566  ignore (GtkMain.Main.init ()) ;
3567  initialize_everything () ;
3568  if !usedb then Mqint.close ();
3569 ;;