helm/gTopLevel/gTopLevel.ml

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