helm/gTopLevel/gTopLevel.ml

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