helm/gTopLevel/gTopLevel.ml

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