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