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 type test_result =
1319    Ok of Cic.term * Cic.metasenv
1320  | Ko
1321  | Uncertain
1322
1323 let disambiguate_input context metasenv dom mk_metasenv_and_expr =
1324  let known_ids,resolve_id = !id_to_uris in
1325  let dom' =
1326   let rec filter =
1327    function
1328       [] -> []
1329     | he::tl ->
1330        if List.mem he known_ids then filter tl else he::(filter tl)
1331   in
1332    filter dom
1333  in
1334   (* for each id in dom' we get the list of uris associated to it *)
1335   let list_of_uris = List.map locate_one_id dom' in
1336   let tests_no =
1337    List.fold_left (fun i uris -> i * List.length uris) 1 list_of_uris
1338   in
1339    if tests_no > 1 then
1340     output_html (outputhtml ())
1341      ("<h1>Disambiguation phase started: " ^
1342        string_of_int tests_no ^ " cases will be tried.") ;
1343   (* and now we compute the list of all possible assignments from *)
1344   (* id to uris that generate well-typed terms                    *)
1345   let resolve_ids =
1346    (* function to test if a partial interpretation is so far correct *)
1347    let test resolve_id residual_dom =
1348     (* We put implicits in place of every identifier that is not *)
1349     (* resolved by resolve_id                                    *)
1350     let resolve_id'' =
1351      let resolve_id' =
1352       function id ->
1353        match resolve_id id with
1354           None -> None
1355         | Some uri -> Some (CicTextualParser0.Uri uri)
1356      in
1357       List.fold_left
1358        (fun f id ->
1359          function id' ->
1360           if id = id' then Some (CicTextualParser0.Implicit) else f id'
1361        ) resolve_id' residual_dom
1362     in
1363      (* and we try to refine the term *)
1364      let saved_status = !CicTextualParser0.metasenv in
1365      let metasenv',expr = mk_metasenv_and_expr resolve_id'' in
1366 (*CSC: Bug here: we do not try to typecheck also the metasenv' *)
1367      (* The parser is imperative ==> we must restore the old status ;-(( *)
1368      CicTextualParser0.metasenv := saved_status ;
1369       try
1370        let term,_,_,metasenv'' =
1371         CicRefine.type_of_aux' metasenv' context expr
1372        in
1373         Ok (term,metasenv'')
1374       with
1375          CicRefine.MutCaseFixAndCofixRefineNotImplemented ->
1376           (try
1377             let term = CicTypeChecker.type_of_aux' metasenv' context expr in
1378              Ok (term,metasenv')
1379            with _ -> Ko
1380           )
1381        | CicRefine.Uncertain _ ->
1382 prerr_endline ("%%% UNCERTAIN!!! " ^ CicPp.ppterm expr) ;
1383           Uncertain
1384        | _ ->
1385 prerr_endline ("%%% PRUNED!!! " ^ CicPp.ppterm expr) ;
1386          Ko
1387    in
1388    let rec aux resolve_id ids list_of_uris =
1389     match ids,list_of_uris with
1390        [],[] ->
1391         (match test resolve_id [] with
1392             Ok (term,metasenv) -> [resolve_id,term,metasenv]
1393           | Ko | Uncertain -> [])
1394      | id::idtl,uris::uristl ->
1395         let rec filter =
1396          function
1397             [] -> []
1398           | uri::uritl ->
1399              let resolve_id' =
1400               function id' -> if id = id' then Some uri else resolve_id id'
1401              in
1402               (match test resolve_id' idtl with
1403                   Ok (term,metasenv) ->
1404                    (* the next three ``if''s are used to avoid the base   *)
1405                    (* case where the term would be refined a second time. *)
1406                    (if uristl = [] then
1407                      [resolve_id',term,metasenv]
1408                     else
1409                      (aux resolve_id' idtl uristl)
1410                    ) @ (filter uritl)
1411                 | Uncertain ->
1412                    (if uristl = [] then []
1413                     else
1414                      (aux resolve_id' idtl uristl)
1415                    ) @ (filter uritl)
1416                 | Ko ->
1417                    filter uritl
1418               )
1419         in
1420          filter uris
1421      | _,_ -> assert false
1422    in
1423     aux resolve_id dom' list_of_uris
1424   in
1425    List.iter
1426     (function (resolve,term,newmetasenv) ->
1427       (* If metasen <> newmetasenv is a normal condition, we should *)
1428       (* be prepared to apply the returned substitution to the      *)
1429       (* whole current proof.                                       *)
1430       if metasenv <> newmetasenv then
1431        begin
1432         prerr_endline
1433          ("+++++ ASSERTION FAILED: " ^
1434           "a refine operation should not modify the metasenv") ;
1435         (* an assert would raise an exception that could be caught *)
1436         exit 1
1437        end
1438     ) resolve_ids ;
1439    let resolve_id',term,metasenv' =
1440     match resolve_ids with
1441        [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
1442      | [resolve_id] -> resolve_id
1443      | _ ->
1444        let choices =
1445         List.map
1446          (function (resolve,_,_) ->
1447            List.map
1448             (function id ->
1449               id,
1450                match resolve id with
1451                   None -> assert false
1452                 | Some uri ->
1453                    match uri with
1454                       CicTextualParser0.ConUri uri
1455                     | CicTextualParser0.VarUri uri ->
1456                        UriManager.string_of_uri uri
1457                     | CicTextualParser0.IndTyUri (uri,tyno) ->
1458                        UriManager.string_of_uri uri ^ "#xpointer(1/" ^
1459                         string_of_int (tyno+1) ^ ")"
1460                     | CicTextualParser0.IndConUri (uri,tyno,consno) ->
1461                        UriManager.string_of_uri uri ^ "#xpointer(1/" ^
1462                         string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^                           ")"
1463             ) dom
1464          ) resolve_ids
1465        in
1466         let index = interactive_interpretation_choice choices in
1467          List.nth resolve_ids index
1468    in
1469     id_to_uris := known_ids @ dom', resolve_id' ;
1470     metasenv',term
1471 ;;
1472
1473 (* A WIDGET TO ENTER CIC TERMS *)
1474
1475 class term_editor ?packing ?width ?height ?isnotempty_callback () =
1476  let input = GEdit.text ~editable:true ?width ?height ?packing () in
1477  let _ =
1478   match isnotempty_callback with
1479      None -> ()
1480    | Some callback ->
1481       ignore(input#connect#changed (function () -> callback (input#length > 0)))
1482  in
1483 object(self)
1484  method coerce = input#coerce
1485  method reset =
1486   input#delete_text 0 input#length
1487  (* CSC: txt is now a string, but should be of type Cic.term *)
1488  method set_term txt =
1489   self#reset ;
1490   ignore ((input#insert_text txt) ~pos:0)
1491  (* CSC: this method should disappear *)
1492  method get_as_string =
1493   input#get_chars 0 input#length
1494  method get_metasenv_and_term ~context ~metasenv =
1495   let name_context =
1496    List.map
1497     (function
1498         Some (n,_) -> Some n
1499       | None -> None
1500     ) context
1501   in
1502    let lexbuf = Lexing.from_string (input#get_chars 0 input#length) in
1503     let dom,mk_metasenv_and_expr =
1504      CicTextualParserContext.main
1505       ~context:name_context ~metasenv CicTextualLexer.token lexbuf
1506     in
1507      disambiguate_input context metasenv dom mk_metasenv_and_expr
1508 end
1509 ;;
1510
1511 (* OTHER FUNCTIONS *)
1512
1513 let locate () =
1514  let inputt = ((rendering_window ())#inputt : term_editor) in
1515  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1516    try
1517     match
1518      GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:"
1519     with
1520        None -> raise NoChoice
1521      | Some input ->
1522         let uri = locate_callback input in
1523          inputt#set_term uri
1524    with
1525     e ->
1526      output_html outputhtml
1527       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1528 ;;
1529
1530
1531 exception UriAlreadyInUse;;
1532 exception NotAUriToAConstant;;
1533
1534 let new_inductive () =
1535  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1536  let output = ((rendering_window ())#output : GMathView.math_view) in
1537  let notebook = (rendering_window ())#notebook in
1538
1539  let chosen = ref false in
1540  let inductive = ref true in
1541  let paramsno = ref 0 in
1542  let get_uri = ref (function _ -> assert false) in
1543  let get_base_uri = ref (function _ -> assert false) in
1544  let get_names = ref (function _ -> assert false) in
1545  let get_types_and_cons = ref (function _ -> assert false) in
1546  let get_context_and_subst = ref (function _ -> assert false) in
1547  let window =
1548   GWindow.window
1549    ~width:600 ~modal:true ~position:`CENTER
1550    ~title:"New Block of Mutual (Co)Inductive Definitions"
1551    ~border_width:2 () in
1552  let vbox = GPack.vbox ~packing:window#add () in
1553  let hbox =
1554   GPack.hbox ~border_width:0
1555    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1556  let _ =
1557   GMisc.label ~text:"Enter the URI for the new block:"
1558    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1559  let uri_entry =
1560   GEdit.entry ~editable:true
1561    ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1562  let hbox0 =
1563   GPack.hbox ~border_width:0
1564    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1565  let _ =
1566   GMisc.label
1567    ~text:
1568      "Enter the number of left parameters in every arity and constructor type:"
1569    ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1570  let paramsno_entry =
1571   GEdit.entry ~editable:true ~text:"0"
1572    ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
1573  let hbox1 =
1574   GPack.hbox ~border_width:0
1575    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1576  let _ =
1577   GMisc.label ~text:"Are the definitions inductive or coinductive?"
1578    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1579  let inductiveb =
1580   GButton.radio_button ~label:"Inductive"
1581    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1582  let coinductiveb =
1583   GButton.radio_button ~label:"Coinductive"
1584    ~group:inductiveb#group
1585    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1586  let hbox2 =
1587   GPack.hbox ~border_width:0
1588    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1589  let _ =
1590   GMisc.label ~text:"Enter the list of the names of the types:"
1591    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1592  let names_entry =
1593   GEdit.entry ~editable:true
1594    ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
1595  let hboxn =
1596   GPack.hbox ~border_width:0
1597    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1598  let okb =
1599   GButton.button ~label:"> Next"
1600    ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1601  let _ = okb#misc#set_sensitive true in
1602  let cancelb =
1603   GButton.button ~label:"Abort"
1604    ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1605  ignore (window#connect#destroy GMain.Main.quit) ;
1606  ignore (cancelb#connect#clicked window#destroy) ;
1607  (* First phase *)
1608  let rec phase1 () =
1609   ignore
1610    (okb#connect#clicked
1611      (function () ->
1612        try
1613         let uristr = "cic:" ^ uri_entry#text in
1614         let namesstr = names_entry#text in
1615         let paramsno' = int_of_string (paramsno_entry#text) in
1616          match Str.split (Str.regexp " +") namesstr with
1617             [] -> assert false
1618           | (he::tl) as names ->
1619              let uri = UriManager.uri_of_string (uristr ^ "/" ^ he ^ ".ind") in
1620               begin
1621                try
1622                 ignore (Getter.resolve uri) ;
1623                 raise UriAlreadyInUse
1624                with
1625                 Getter.Unresolved ->
1626                  get_uri := (function () -> uri) ;
1627                  get_names := (function () -> names) ;
1628                  inductive := inductiveb#active ;
1629                  paramsno := paramsno' ;
1630                  phase2 ()
1631               end
1632        with
1633         e ->
1634          output_html outputhtml
1635           ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1636      ))
1637  (* Second phase *)
1638  and phase2 () =
1639   let type_widgets =
1640    List.map
1641     (function name ->
1642       let frame =
1643        GBin.frame ~label:name
1644         ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
1645       let vbox = GPack.vbox ~packing:frame#add () in
1646       let hbox = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false) () in
1647       let _ =
1648        GMisc.label ~text:("Enter its type:")
1649         ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1650       let scrolled_window =
1651        GBin.scrolled_window ~border_width:5
1652         ~packing:(vbox#pack ~expand:true ~padding:0) () in
1653       let newinputt =
1654        new term_editor ~width:400 ~height:20 ~packing:scrolled_window#add ()
1655         ~isnotempty_callback:
1656          (function b ->
1657            (*non_empty_type := b ;*)
1658            okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*)
1659       in
1660       let hbox =
1661        GPack.hbox ~border_width:0
1662         ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1663       let _ =
1664        GMisc.label ~text:("Enter the list of its constructors:")
1665         ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1666       let cons_names_entry =
1667        GEdit.entry ~editable:true
1668         ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1669       (newinputt,cons_names_entry)
1670     ) (!get_names ())
1671   in
1672    vbox#remove hboxn#coerce ;
1673    let hboxn =
1674     GPack.hbox ~border_width:0
1675      ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1676    let okb =
1677     GButton.button ~label:"> Next"
1678      ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1679    let cancelb =
1680     GButton.button ~label:"Abort"
1681      ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1682    ignore (cancelb#connect#clicked window#destroy) ;
1683    ignore
1684     (okb#connect#clicked
1685       (function () ->
1686         try
1687          let names = !get_names () in
1688          let types_and_cons =
1689           List.map2
1690            (fun name (newinputt,cons_names_entry) ->
1691              let consnamesstr = cons_names_entry#text in
1692              let cons_names = Str.split (Str.regexp " +") consnamesstr in
1693              let metasenv,expr =
1694               newinputt#get_metasenv_and_term ~context:[] ~metasenv:[]
1695              in
1696               match metasenv with
1697                  [] -> expr,cons_names
1698                | _ -> raise AmbiguousInput
1699            ) names type_widgets
1700          in
1701           let uri = !get_uri () in
1702           let _ =
1703            (* Let's see if so far the definition is well-typed *)
1704            let params = [] in
1705            let paramsno = 0 in
1706            (* To test if the arities of the inductive types are well *)
1707            (* typed, we check the inductive block definition where   *)
1708            (* no constructor is given to each type.                  *)
1709            let tys =
1710             List.map2
1711              (fun name (ty,cons) -> (name, !inductive, ty, []))
1712              names types_and_cons
1713            in
1714             CicTypeChecker.typecheck_mutual_inductive_defs uri
1715              (tys,params,paramsno)
1716           in
1717            get_context_and_subst :=
1718             (function () ->
1719               let i = ref 0 in
1720                List.fold_left2
1721                 (fun (context,subst) name (ty,_) ->
1722                   let res =
1723                    (Some (Cic.Name name, Cic.Decl ty))::context,
1724                     (Cic.MutInd (uri,!i,[]))::subst
1725                   in
1726                    incr i ; res
1727                 ) ([],[]) names types_and_cons) ;
1728            let types_and_cons' =
1729             List.map2
1730              (fun name (ty,cons) -> (name, !inductive, ty, phase3 name cons))
1731              names types_and_cons
1732            in
1733             get_types_and_cons := (function () -> types_and_cons') ;
1734             chosen := true ;
1735             window#destroy ()
1736         with
1737          e ->
1738           output_html outputhtml
1739            ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1740       ))
1741  (* Third phase *)
1742  and phase3 name cons =
1743   let get_cons_types = ref (function () -> assert false) in
1744   let window2 =
1745    GWindow.window
1746     ~width:600 ~modal:true ~position:`CENTER
1747     ~title:(name ^ " Constructors")
1748     ~border_width:2 () in
1749   let vbox = GPack.vbox ~packing:window2#add () in
1750   let cons_type_widgets =
1751    List.map
1752     (function consname ->
1753       let hbox =
1754        GPack.hbox ~border_width:0
1755         ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1756       let _ =
1757        GMisc.label ~text:("Enter the type of " ^ consname ^ ":")
1758         ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1759       let scrolled_window =
1760        GBin.scrolled_window ~border_width:5
1761         ~packing:(vbox#pack ~expand:true ~padding:0) () in
1762       let newinputt =
1763        new term_editor ~width:400 ~height:20 ~packing:scrolled_window#add ()
1764         ~isnotempty_callback:
1765          (function b ->
1766            (* (*non_empty_type := b ;*)
1767            okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*) *)())
1768       in
1769        newinputt
1770     ) cons in
1771   let hboxn =
1772    GPack.hbox ~border_width:0
1773     ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1774   let okb =
1775    GButton.button ~label:"> Next"
1776     ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1777   let _ = okb#misc#set_sensitive true in
1778   let cancelb =
1779    GButton.button ~label:"Abort"
1780     ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1781   ignore (window2#connect#destroy GMain.Main.quit) ;
1782   ignore (cancelb#connect#clicked window2#destroy) ;
1783   ignore
1784    (okb#connect#clicked
1785      (function () ->
1786        try
1787         chosen := true ;
1788         let context,subst= !get_context_and_subst () in
1789         let cons_types =
1790          List.map2
1791           (fun name inputt ->
1792             let metasenv,expr =
1793              inputt#get_metasenv_and_term ~context ~metasenv:[]
1794             in
1795              match metasenv with
1796                 [] ->
1797                  let undebrujined_expr =
1798                   List.fold_left
1799                    (fun expr t -> CicSubstitution.subst t expr) expr subst
1800                  in
1801                   name, undebrujined_expr
1802               | _ -> raise AmbiguousInput
1803           ) cons cons_type_widgets
1804         in
1805          get_cons_types := (function () -> cons_types) ;
1806          window2#destroy ()
1807        with
1808         e ->
1809          output_html outputhtml
1810           ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1811      )) ;
1812   window2#show () ;
1813   GMain.Main.main () ;
1814   let okb_pressed = !chosen in
1815    chosen := false ;
1816    if (not okb_pressed) then
1817     begin
1818      window#destroy () ;
1819      assert false (* The control never reaches this point *)
1820     end
1821    else
1822     (!get_cons_types ())
1823  in
1824   phase1 () ;
1825   (* No more phases left or Abort pressed *)
1826   window#show () ;
1827   GMain.Main.main () ;
1828   window#destroy () ;
1829   if !chosen then
1830    try
1831     let uri = !get_uri () in
1832 (*CSC: Da finire *)
1833     let params = [] in
1834     let tys = !get_types_and_cons () in
1835      let obj = Cic.InductiveDefinition tys params !paramsno in
1836       begin
1837        try
1838         prerr_endline (CicPp.ppobj obj) ;
1839         CicTypeChecker.typecheck_mutual_inductive_defs uri
1840          (tys,params,!paramsno) ;
1841         with
1842          e ->
1843           prerr_endline "Offending mutual (co)inductive type declaration:" ;
1844           prerr_endline (CicPp.ppobj obj) ;
1845       end ;
1846       (* We already know that obj is well-typed. We need to add it to the  *)
1847       (* environment in order to compute the inner-types without having to *)
1848       (* debrujin it or having to modify lots of other functions to avoid  *)
1849       (* asking the environment for the MUTINDs we are defining now.       *)
1850       CicEnvironment.put_inductive_definition uri obj ;
1851       save_obj uri obj ;
1852       show_in_show_window_obj uri obj
1853    with
1854     e ->
1855      output_html outputhtml
1856       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1857 ;;
1858
1859 let new_proof () =
1860  let inputt = ((rendering_window ())#inputt : term_editor) in
1861  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1862  let output = ((rendering_window ())#output : GMathView.math_view) in
1863  let notebook = (rendering_window ())#notebook in
1864
1865  let chosen = ref false in
1866  let get_metasenv_and_term = ref (function _ -> assert false) in
1867  let get_uri = ref (function _ -> assert false) in
1868  let non_empty_type = ref false in
1869  let window =
1870   GWindow.window
1871    ~width:600 ~modal:true ~title:"New Proof or Definition"
1872    ~border_width:2 () in
1873  let vbox = GPack.vbox ~packing:window#add () in
1874  let hbox =
1875   GPack.hbox ~border_width:0
1876    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1877  let _ =
1878   GMisc.label ~text:"Enter the URI for the new theorem or definition:"
1879    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1880  let uri_entry =
1881   GEdit.entry ~editable:true
1882    ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1883  let hbox1 =
1884   GPack.hbox ~border_width:0
1885    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1886  let _ =
1887   GMisc.label ~text:"Enter the theorem or definition type:"
1888    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1889  let scrolled_window =
1890   GBin.scrolled_window ~border_width:5
1891    ~packing:(vbox#pack ~expand:true ~padding:0) () in
1892  (* the content of the scrolled_window is moved below (see comment) *)
1893  let hbox =
1894   GPack.hbox ~border_width:0
1895    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1896  let okb =
1897   GButton.button ~label:"Ok"
1898    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1899  let _ = okb#misc#set_sensitive false in
1900  let cancelb =
1901   GButton.button ~label:"Cancel"
1902    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1903  (* moved here to have visibility of the ok button *)
1904  let newinputt =
1905   new term_editor ~width:400 ~height:100 ~packing:scrolled_window#add ()
1906    ~isnotempty_callback:
1907     (function b ->
1908       non_empty_type := b ;
1909       okb#misc#set_sensitive (b && uri_entry#text <> ""))
1910  in
1911  let _ =
1912   newinputt#set_term inputt#get_as_string ;
1913   inputt#reset in
1914  let _ =
1915   uri_entry#connect#changed
1916    (function () ->
1917      okb#misc#set_sensitive (!non_empty_type && uri_entry#text <> ""))
1918  in
1919  ignore (window#connect#destroy GMain.Main.quit) ;
1920  ignore (cancelb#connect#clicked window#destroy) ;
1921  ignore
1922   (okb#connect#clicked
1923     (function () ->
1924       chosen := true ;
1925       try
1926        let metasenv,parsed = newinputt#get_metasenv_and_term [] [] in
1927        let uristr = "cic:" ^ uri_entry#text in
1928        let uri = UriManager.uri_of_string uristr in
1929         if String.sub uristr (String.length uristr - 4) 4 <> ".con" then
1930          raise NotAUriToAConstant
1931         else
1932          begin
1933           try
1934            ignore (Getter.resolve uri) ;
1935            raise UriAlreadyInUse
1936           with
1937            Getter.Unresolved ->
1938             get_metasenv_and_term := (function () -> metasenv,parsed) ;
1939             get_uri := (function () -> uri) ;
1940             window#destroy ()
1941          end
1942       with
1943        e ->
1944         output_html outputhtml
1945          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1946   )) ;
1947  window#show () ;
1948  GMain.Main.main () ;
1949  if !chosen then
1950   try
1951    let metasenv,expr = !get_metasenv_and_term () in
1952     let _  = CicTypeChecker.type_of_aux' metasenv [] expr in
1953      ProofEngine.proof :=
1954       Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
1955      ProofEngine.goal := Some 1 ;
1956      refresh_sequent notebook ;
1957      refresh_proof output ;
1958      !save_set_sensitive true ;
1959      inputt#reset
1960   with
1961      RefreshSequentException e ->
1962       output_html outputhtml
1963        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1964         "sequent: " ^ Printexc.to_string e ^ "</h1>")
1965    | RefreshProofException e ->
1966       output_html outputhtml
1967        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1968         "proof: " ^ Printexc.to_string e ^ "</h1>")
1969    | e ->
1970       output_html outputhtml
1971        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1972 ;;
1973
1974 let check_term_in_scratch scratch_window metasenv context expr =
1975  try
1976   let ty = CicTypeChecker.type_of_aux' metasenv context expr in
1977    let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
1978     scratch_window#show () ;
1979     scratch_window#mmlwidget#load_tree ~dom:mml
1980  with
1981   e ->
1982    print_endline ("? " ^ CicPp.ppterm expr) ;
1983    raise e
1984 ;;
1985
1986 let check scratch_window () =
1987  let inputt = ((rendering_window ())#inputt : term_editor) in
1988  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1989   let metasenv =
1990    match !ProofEngine.proof with
1991       None -> []
1992     | Some (_,metasenv,_,_) -> metasenv
1993   in
1994   let context =
1995    match !ProofEngine.goal with
1996       None -> []
1997     | Some metano ->
1998        let (_,canonical_context,_) =
1999         List.find (function (m,_,_) -> m=metano) metasenv
2000        in
2001         canonical_context
2002   in
2003    try
2004     let metasenv',expr = inputt#get_metasenv_and_term context metasenv in
2005      check_term_in_scratch scratch_window metasenv' context expr
2006    with
2007     e ->
2008      output_html outputhtml
2009       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2010 ;;
2011
2012
2013 (***********************)
2014 (*       TACTICS       *)
2015 (***********************)
2016
2017 let call_tactic tactic () =
2018  let notebook = (rendering_window ())#notebook in
2019  let output = ((rendering_window ())#output : GMathView.math_view) in
2020  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2021  let savedproof = !ProofEngine.proof in
2022  let savedgoal  = !ProofEngine.goal in
2023   begin
2024    try
2025     tactic () ;
2026     refresh_sequent notebook ;
2027     refresh_proof output
2028    with
2029       RefreshSequentException e ->
2030        output_html outputhtml
2031         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2032          "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2033        ProofEngine.proof := savedproof ;
2034        ProofEngine.goal := savedgoal ;
2035        refresh_sequent notebook
2036     | RefreshProofException e ->
2037        output_html outputhtml
2038         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2039          "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2040        ProofEngine.proof := savedproof ;
2041        ProofEngine.goal := savedgoal ;
2042        refresh_sequent notebook ;
2043        refresh_proof output
2044     | e ->
2045        output_html outputhtml
2046         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2047        ProofEngine.proof := savedproof ;
2048        ProofEngine.goal := savedgoal ;
2049   end
2050 ;;
2051
2052 let call_tactic_with_input tactic () =
2053  let notebook = (rendering_window ())#notebook in
2054  let output = ((rendering_window ())#output : GMathView.math_view) in
2055  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2056  let inputt = ((rendering_window ())#inputt : term_editor) in
2057  let savedproof = !ProofEngine.proof in
2058  let savedgoal  = !ProofEngine.goal in
2059   let uri,metasenv,bo,ty =
2060    match !ProofEngine.proof with
2061       None -> assert false
2062     | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
2063   in
2064    let canonical_context =
2065     match !ProofEngine.goal with
2066        None -> assert false
2067      | Some metano ->
2068         let (_,canonical_context,_) =
2069          List.find (function (m,_,_) -> m=metano) metasenv
2070         in
2071          canonical_context
2072    in
2073     try
2074      let metasenv',expr =
2075       inputt#get_metasenv_and_term canonical_context metasenv
2076      in
2077       ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
2078       tactic expr ;
2079       refresh_sequent notebook ;
2080       refresh_proof output ;
2081       inputt#reset
2082     with
2083        RefreshSequentException e ->
2084         output_html outputhtml
2085          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2086           "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2087         ProofEngine.proof := savedproof ;
2088         ProofEngine.goal := savedgoal ;
2089         refresh_sequent notebook
2090      | RefreshProofException e ->
2091         output_html outputhtml
2092          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2093           "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2094         ProofEngine.proof := savedproof ;
2095         ProofEngine.goal := savedgoal ;
2096         refresh_sequent notebook ;
2097         refresh_proof output
2098      | e ->
2099         output_html outputhtml
2100          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2101         ProofEngine.proof := savedproof ;
2102         ProofEngine.goal := savedgoal ;
2103 ;;
2104
2105 let call_tactic_with_goal_input tactic () =
2106  let module L = LogicalOperations in
2107  let module G = Gdome in
2108   let notebook = (rendering_window ())#notebook in
2109   let output = ((rendering_window ())#output : GMathView.math_view) in
2110   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2111   let savedproof = !ProofEngine.proof in
2112   let savedgoal  = !ProofEngine.goal in
2113    match notebook#proofw#get_selection with
2114      Some node ->
2115       let xpath =
2116        ((node : Gdome.element)#getAttributeNS
2117          ~namespaceURI:helmns
2118          ~localName:(G.domString "xref"))#to_string
2119       in
2120        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2121        else
2122         begin
2123          try
2124           match !current_goal_infos with
2125              Some (ids_to_terms, ids_to_father_ids,_) ->
2126               let id = xpath in
2127                tactic (Hashtbl.find ids_to_terms id) ;
2128                refresh_sequent notebook ;
2129                refresh_proof output
2130            | None -> assert false (* "ERROR: No current term!!!" *)
2131          with
2132             RefreshSequentException e ->
2133              output_html outputhtml
2134               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2135                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2136              ProofEngine.proof := savedproof ;
2137              ProofEngine.goal := savedgoal ;
2138              refresh_sequent notebook
2139           | RefreshProofException e ->
2140              output_html outputhtml
2141               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2142                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2143              ProofEngine.proof := savedproof ;
2144              ProofEngine.goal := savedgoal ;
2145              refresh_sequent notebook ;
2146              refresh_proof output
2147           | e ->
2148              output_html outputhtml
2149               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2150              ProofEngine.proof := savedproof ;
2151              ProofEngine.goal := savedgoal ;
2152         end
2153    | None ->
2154       output_html outputhtml
2155        ("<h1 color=\"red\">No term selected</h1>")
2156 ;;
2157
2158 let call_tactic_with_input_and_goal_input tactic () =
2159  let module L = LogicalOperations in
2160  let module G = Gdome in
2161   let notebook = (rendering_window ())#notebook in
2162   let output = ((rendering_window ())#output : GMathView.math_view) in
2163   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2164   let inputt = ((rendering_window ())#inputt : term_editor) in
2165   let savedproof = !ProofEngine.proof in
2166   let savedgoal  = !ProofEngine.goal in
2167    match notebook#proofw#get_selection with
2168      Some node ->
2169       let xpath =
2170        ((node : Gdome.element)#getAttributeNS
2171          ~namespaceURI:helmns
2172          ~localName:(G.domString "xref"))#to_string
2173       in
2174        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2175        else
2176         begin
2177          try
2178           match !current_goal_infos with
2179              Some (ids_to_terms, ids_to_father_ids,_) ->
2180               let id = xpath in
2181                let uri,metasenv,bo,ty =
2182                 match !ProofEngine.proof with
2183                    None -> assert false
2184                  | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
2185                in
2186                 let canonical_context =
2187                  match !ProofEngine.goal with
2188                     None -> assert false
2189                   | Some metano ->
2190                      let (_,canonical_context,_) =
2191                       List.find (function (m,_,_) -> m=metano) metasenv
2192                      in
2193                       canonical_context in
2194                 let (metasenv',expr) =
2195                  inputt#get_metasenv_and_term canonical_context metasenv
2196                 in
2197                  ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
2198                  tactic ~goal_input:(Hashtbl.find ids_to_terms id)
2199                   ~input:expr ;
2200                  refresh_sequent notebook ;
2201                  refresh_proof output ;
2202                  inputt#reset
2203            | None -> assert false (* "ERROR: No current term!!!" *)
2204          with
2205             RefreshSequentException e ->
2206              output_html outputhtml
2207               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2208                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2209              ProofEngine.proof := savedproof ;
2210              ProofEngine.goal := savedgoal ;
2211              refresh_sequent notebook
2212           | RefreshProofException e ->
2213              output_html outputhtml
2214               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2215                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2216              ProofEngine.proof := savedproof ;
2217              ProofEngine.goal := savedgoal ;
2218              refresh_sequent notebook ;
2219              refresh_proof output
2220           | e ->
2221              output_html outputhtml
2222               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2223              ProofEngine.proof := savedproof ;
2224              ProofEngine.goal := savedgoal ;
2225         end
2226    | None ->
2227       output_html outputhtml
2228        ("<h1 color=\"red\">No term selected</h1>")
2229 ;;
2230
2231 let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
2232  let module L = LogicalOperations in
2233  let module G = Gdome in
2234   let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in
2235   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2236   let savedproof = !ProofEngine.proof in
2237   let savedgoal  = !ProofEngine.goal in
2238    match mmlwidget#get_selection with
2239      Some node ->
2240       let xpath =
2241        ((node : Gdome.element)#getAttributeNS
2242          ~namespaceURI:helmns
2243          ~localName:(G.domString "xref"))#to_string
2244       in
2245        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2246        else
2247         begin
2248          try
2249           match !current_scratch_infos with
2250              (* term is the whole goal in the scratch_area *)
2251              Some (term,ids_to_terms, ids_to_father_ids,_) ->
2252               let id = xpath in
2253                let expr = tactic term (Hashtbl.find ids_to_terms id) in
2254                 let mml = mml_of_cic_term 111 expr in
2255                  scratch_window#show () ;
2256                  scratch_window#mmlwidget#load_tree ~dom:mml
2257            | None -> assert false (* "ERROR: No current term!!!" *)
2258          with
2259           e ->
2260            output_html outputhtml
2261             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2262         end
2263    | None ->
2264       output_html outputhtml
2265        ("<h1 color=\"red\">No term selected</h1>")
2266 ;;
2267
2268 let call_tactic_with_hypothesis_input tactic () =
2269  let module L = LogicalOperations in
2270  let module G = Gdome in
2271   let notebook = (rendering_window ())#notebook in
2272   let output = ((rendering_window ())#output : GMathView.math_view) in
2273   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2274   let savedproof = !ProofEngine.proof in
2275   let savedgoal  = !ProofEngine.goal in
2276    match notebook#proofw#get_selection with
2277      Some node ->
2278       let xpath =
2279        ((node : Gdome.element)#getAttributeNS
2280          ~namespaceURI:helmns
2281          ~localName:(G.domString "xref"))#to_string
2282       in
2283        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2284        else
2285         begin
2286          try
2287           match !current_goal_infos with
2288              Some (_,_,ids_to_hypotheses) ->
2289               let id = xpath in
2290                tactic (Hashtbl.find ids_to_hypotheses id) ;
2291                refresh_sequent notebook ;
2292                refresh_proof output
2293            | None -> assert false (* "ERROR: No current term!!!" *)
2294          with
2295             RefreshSequentException e ->
2296              output_html outputhtml
2297               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2298                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2299              ProofEngine.proof := savedproof ;
2300              ProofEngine.goal := savedgoal ;
2301              refresh_sequent notebook
2302           | RefreshProofException e ->
2303              output_html outputhtml
2304               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2305                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2306              ProofEngine.proof := savedproof ;
2307              ProofEngine.goal := savedgoal ;
2308              refresh_sequent notebook ;
2309              refresh_proof output
2310           | e ->
2311              output_html outputhtml
2312               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2313              ProofEngine.proof := savedproof ;
2314              ProofEngine.goal := savedgoal ;
2315         end
2316    | None ->
2317       output_html outputhtml
2318        ("<h1 color=\"red\">No term selected</h1>")
2319 ;;
2320
2321
2322 let intros = call_tactic ProofEngine.intros;;
2323 let exact = call_tactic_with_input ProofEngine.exact;;
2324 let apply = call_tactic_with_input ProofEngine.apply;;
2325 let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl;;
2326 let elimtype = call_tactic_with_input ProofEngine.elim_type;;
2327 let whd = call_tactic_with_goal_input ProofEngine.whd;;
2328 let reduce = call_tactic_with_goal_input ProofEngine.reduce;;
2329 let simpl = call_tactic_with_goal_input ProofEngine.simpl;;
2330 let fold_whd = call_tactic_with_input ProofEngine.fold_whd;;
2331 let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce;;
2332 let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl;;
2333 let cut = call_tactic_with_input ProofEngine.cut;;
2334 let change = call_tactic_with_input_and_goal_input ProofEngine.change;;
2335 let letin = call_tactic_with_input ProofEngine.letin;;
2336 let ring = call_tactic ProofEngine.ring;;
2337 let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody;;
2338 let clear = call_tactic_with_hypothesis_input ProofEngine.clear;;
2339 let fourier = call_tactic ProofEngine.fourier;;
2340 let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl;;
2341 let rewritebacksimpl = call_tactic_with_input ProofEngine.rewrite_back_simpl;;
2342 let replace = call_tactic_with_input_and_goal_input ProofEngine.replace;;
2343 let reflexivity = call_tactic ProofEngine.reflexivity;;
2344 let symmetry = call_tactic ProofEngine.symmetry;;
2345 let transitivity = call_tactic_with_input ProofEngine.transitivity;;
2346 let exists = call_tactic ProofEngine.exists;;
2347 let split = call_tactic ProofEngine.split;;
2348 let left = call_tactic ProofEngine.left;;
2349 let right = call_tactic ProofEngine.right;;
2350 let assumption = call_tactic ProofEngine.assumption;;
2351 let generalize = call_tactic_with_goal_input ProofEngine.generalize;;
2352 let absurd = call_tactic_with_input ProofEngine.absurd;;
2353 let contradiction = call_tactic ProofEngine.contradiction;;
2354 (* Galla chiede: come dare alla tattica la lista di termini da decomporre?
2355 let decompose = call_tactic_with_input_and_goal_input ProofEngine.decompose;;
2356 *)
2357
2358 let whd_in_scratch scratch_window =
2359  call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
2360   scratch_window
2361 ;;
2362 let reduce_in_scratch scratch_window =
2363  call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch
2364   scratch_window
2365 ;;
2366 let simpl_in_scratch scratch_window =
2367  call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch
2368   scratch_window
2369 ;;
2370
2371
2372
2373 (**********************)
2374 (*   END OF TACTICS   *)
2375 (**********************)
2376
2377
2378 let show () =
2379  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2380   try
2381    show_in_show_window_uri (input_or_locate_uri ~title:"Show")
2382   with
2383    e ->
2384     output_html outputhtml
2385      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2386 ;;
2387
2388 exception NotADefinition;;
2389
2390 let open_ () =
2391  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2392  let output = ((rendering_window ())#output : GMathView.math_view) in
2393  let notebook = (rendering_window ())#notebook in
2394    try
2395     let uri = input_or_locate_uri ~title:"Open" in
2396      CicTypeChecker.typecheck uri ;
2397      let metasenv,bo,ty =
2398       match CicEnvironment.get_cooked_obj uri with
2399          Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
2400        | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
2401        | Cic.Constant _
2402        | Cic.Variable _
2403        | Cic.InductiveDefinition _ -> raise NotADefinition
2404      in
2405       ProofEngine.proof :=
2406        Some (uri, metasenv, bo, ty) ;
2407       ProofEngine.goal := None ;
2408       refresh_sequent notebook ;
2409       refresh_proof output
2410    with
2411       RefreshSequentException e ->
2412        output_html outputhtml
2413         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2414          "sequent: " ^ Printexc.to_string e ^ "</h1>")
2415     | RefreshProofException e ->
2416        output_html outputhtml
2417         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2418          "proof: " ^ Printexc.to_string e ^ "</h1>")
2419     | e ->
2420        output_html outputhtml
2421         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2422 ;;
2423
2424 let show_query_results results =
2425  let window =
2426   GWindow.window
2427    ~modal:false ~title:"Query results." ~border_width:2 () in
2428  let vbox = GPack.vbox ~packing:window#add () in
2429  let hbox =
2430   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2431  let lMessage =
2432   GMisc.label
2433    ~text:"Click on a URI to show that object"
2434    ~packing:hbox#add () in
2435  let scrolled_window =
2436   GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
2437    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2438  let clist = GList.clist ~columns:1 ~packing:scrolled_window#add () in
2439   ignore
2440    (List.map
2441      (function (uri,_) ->
2442        let n =
2443         clist#append [uri]
2444        in
2445         clist#set_row ~selectable:false n
2446      ) results
2447    ) ;
2448   clist#columns_autosize () ;
2449   ignore
2450    (clist#connect#select_row
2451      (fun ~row ~column ~event ->
2452        let (uristr,_) = List.nth results row in
2453         match
2454          cic_textual_parser_uri_of_string
2455           (wrong_xpointer_format_from_wrong_xpointer_format' uristr)
2456         with
2457            CicTextualParser0.ConUri uri
2458          | CicTextualParser0.VarUri uri
2459          | CicTextualParser0.IndTyUri (uri,_)
2460          | CicTextualParser0.IndConUri (uri,_,_) ->
2461             show_in_show_window_uri uri
2462      )
2463    ) ;
2464   window#show ()
2465 ;;
2466
2467 let refine_constraints (must_obj,must_rel,must_sort) =
2468  let chosen = ref false in
2469  let use_only = ref false in
2470  let window =
2471   GWindow.window
2472    ~modal:true ~title:"Constraints refinement."
2473    ~width:800 ~border_width:2 () in
2474  let vbox = GPack.vbox ~packing:window#add () in
2475  let hbox =
2476   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2477  let lMessage =
2478   GMisc.label
2479    ~text: "\"Only\" constraints can be enforced or not."
2480    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2481  let onlyb =
2482   GButton.toggle_button ~label:"Enforce \"only\" constraints"
2483    ~active:false ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2484  in
2485   ignore
2486    (onlyb#connect#toggled (function () -> use_only := onlyb#active)) ;
2487  (* Notebook for the constraints choice *)
2488  let notebook =
2489   GPack.notebook ~scrollable:true
2490    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2491  (* Rel constraints *)
2492  let label =
2493   GMisc.label
2494    ~text: "Constraints on Rels" () in
2495  let vbox' =
2496   GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
2497    () in
2498  let hbox =
2499   GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2500  let lMessage =
2501   GMisc.label
2502    ~text: "You can now specify the constraints on Rels."
2503    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2504  let expected_height = 25 * (List.length must_rel + 2) in
2505  let height = if expected_height > 400 then 400 else expected_height in
2506  let scrolled_window =
2507   GBin.scrolled_window ~border_width:10 ~height ~width:600
2508    ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
2509  let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
2510  let rel_constraints =
2511   List.map
2512    (function (position,depth) ->
2513      let hbox =
2514       GPack.hbox
2515        ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
2516      let lMessage =
2517       GMisc.label
2518        ~text:position
2519        ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2520      match depth with
2521         None -> position, ref None
2522       | Some depth' ->
2523          let mutable_ref = ref (Some depth') in
2524          let depthb =
2525           GButton.toggle_button
2526            ~label:("depth = " ^ string_of_int depth') ~active:true
2527            ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2528          in
2529           ignore
2530            (depthb#connect#toggled
2531              (function () ->
2532                let sel_depth = if depthb#active then Some depth' else None in
2533                 mutable_ref := sel_depth
2534             )) ;
2535           position, mutable_ref
2536    ) must_rel in
2537  (* Sort constraints *)
2538  let label =
2539   GMisc.label
2540    ~text: "Constraints on Sorts" () in
2541  let vbox' =
2542   GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
2543    () in
2544  let hbox =
2545   GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2546  let lMessage =
2547   GMisc.label
2548    ~text: "You can now specify the constraints on Sorts."
2549    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2550  let expected_height = 25 * (List.length must_sort + 2) in
2551  let height = if expected_height > 400 then 400 else expected_height in
2552  let scrolled_window =
2553   GBin.scrolled_window ~border_width:10 ~height ~width:600
2554    ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
2555  let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
2556  let sort_constraints =
2557   List.map
2558    (function (position,depth,sort) ->
2559      let hbox =
2560       GPack.hbox
2561        ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
2562      let lMessage =
2563       GMisc.label
2564        ~text:(sort ^ " " ^ position)
2565        ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2566      match depth with
2567         None -> position, ref None, sort
2568       | Some depth' ->
2569          let mutable_ref = ref (Some depth') in
2570          let depthb =
2571           GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
2572            ~active:true
2573            ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2574          in
2575           ignore
2576            (depthb#connect#toggled
2577              (function () ->
2578                let sel_depth = if depthb#active then Some depth' else None in
2579                 mutable_ref := sel_depth
2580             )) ;
2581           position, mutable_ref, sort
2582    ) must_sort in
2583  (* Obj constraints *)
2584  let label =
2585   GMisc.label
2586    ~text: "Constraints on constants" () in
2587  let vbox' =
2588   GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
2589    () in
2590  let hbox =
2591   GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2592  let lMessage =
2593   GMisc.label
2594    ~text: "You can now specify the constraints on constants."
2595    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2596  let expected_height = 25 * (List.length must_obj + 2) in
2597  let height = if expected_height > 400 then 400 else expected_height in
2598  let scrolled_window =
2599   GBin.scrolled_window ~border_width:10 ~height ~width:600
2600    ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
2601  let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
2602  let obj_constraints =
2603   List.map
2604    (function (uri,position,depth) ->
2605      let hbox =
2606       GPack.hbox
2607        ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
2608      let lMessage =
2609       GMisc.label
2610        ~text:(uri ^ " " ^ position)
2611        ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2612      match depth with
2613         None -> uri, position, ref None
2614       | Some depth' ->
2615          let mutable_ref = ref (Some depth') in
2616          let depthb =
2617           GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
2618            ~active:true
2619            ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2620          in
2621           ignore
2622            (depthb#connect#toggled
2623              (function () ->
2624                let sel_depth = if depthb#active then Some depth' else None in
2625                 mutable_ref := sel_depth
2626             )) ;
2627           uri, position, mutable_ref
2628    ) must_obj in
2629  (* Confirm/abort buttons *)
2630  let hbox =
2631   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2632  let okb =
2633   GButton.button ~label:"Ok"
2634    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2635  let cancelb =
2636   GButton.button ~label:"Abort"
2637    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2638  in
2639   ignore (window#connect#destroy GMain.Main.quit) ;
2640   ignore (cancelb#connect#clicked window#destroy) ;
2641   ignore
2642    (okb#connect#clicked (function () -> chosen := true ; window#destroy ()));
2643   window#set_position `CENTER ;
2644   window#show () ;
2645   GMain.Main.main () ;
2646   if !chosen then
2647    let chosen_must_rel =
2648     List.map
2649      (function (position,ref_depth) -> position,!ref_depth) rel_constraints in
2650    let chosen_must_sort =
2651     List.map
2652      (function (position,ref_depth,sort) -> position,!ref_depth,sort)
2653      sort_constraints
2654    in
2655    let chosen_must_obj =
2656     List.map
2657      (function (uri,position,ref_depth) -> uri,position,!ref_depth)
2658      obj_constraints
2659    in
2660     (chosen_must_obj,chosen_must_rel,chosen_must_sort),
2661      (if !use_only then
2662 (*CSC: ???????????????????????? I assume that must and only are the same... *)
2663        Some chosen_must_obj,Some chosen_must_rel,Some chosen_must_sort
2664       else
2665        None,None,None
2666      )
2667   else
2668    raise NoChoice
2669 ;;
2670
2671 let completeSearchPattern () =
2672  let inputt = ((rendering_window ())#inputt : term_editor) in
2673  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2674   try
2675    let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
2676    let must = MQueryLevels2.get_constraints expr in
2677    let must',only = refine_constraints must in
2678    let results = MQueryGenerator.searchPattern must' only in
2679     show_query_results results
2680   with
2681    e ->
2682     output_html outputhtml
2683      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2684 ;;
2685
2686 let insertQuery () =
2687  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2688   try
2689    let chosen = ref None in
2690    let window =
2691     GWindow.window
2692      ~modal:true ~title:"Insert Query (Experts Only)" ~border_width:2 () in
2693    let vbox = GPack.vbox ~packing:window#add () in
2694    let label =
2695     GMisc.label ~text:"Insert Query. For Experts Only."
2696      ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2697    let scrolled_window =
2698     GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
2699      ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2700    let input = GEdit.text ~editable:true
2701     ~packing:scrolled_window#add () in
2702    let hbox =
2703     GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2704    let okb =
2705     GButton.button ~label:"Ok"
2706      ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2707    let loadb =
2708     GButton.button ~label:"Load from file..."
2709      ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2710    let cancelb =
2711     GButton.button ~label:"Abort"
2712      ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2713    ignore (window#connect#destroy GMain.Main.quit) ;
2714    ignore (cancelb#connect#clicked window#destroy) ;
2715    ignore
2716     (okb#connect#clicked
2717       (function () ->
2718         chosen := Some (input#get_chars 0 input#length) ; window#destroy ())) ;
2719    ignore
2720     (loadb#connect#clicked
2721       (function () ->
2722         match
2723          GToolbox.select_file ~title:"Select Query File" ()
2724         with
2725            None -> ()
2726          | Some filename ->
2727             let inch = open_in filename in
2728              let rec read_file () =
2729               try
2730                let line = input_line inch in
2731                 line ^ "\n" ^ read_file ()
2732               with
2733                End_of_file -> ""
2734              in
2735               let text = read_file () in
2736                input#delete_text 0 input#length ;
2737                ignore (input#insert_text text ~pos:0))) ;
2738    window#set_position `CENTER ;
2739    window#show () ;
2740    GMain.Main.main () ;
2741    match !chosen with
2742       None -> ()
2743     | Some q ->
2744        let results =
2745         Mqint.execute (MQueryUtil.query_of_text (Lexing.from_string q))
2746        in
2747         show_query_results results
2748   with
2749    e ->
2750     output_html outputhtml
2751      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2752 ;;
2753
2754 let choose_must list_of_must only =
2755  let chosen = ref None in
2756  let user_constraints = ref [] in
2757  let window =
2758   GWindow.window
2759    ~modal:true ~title:"Query refinement." ~border_width:2 () in
2760  let vbox = GPack.vbox ~packing:window#add () in
2761  let hbox =
2762   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2763  let lMessage =
2764   GMisc.label
2765    ~text:
2766     ("You can now specify the genericity of the query. " ^
2767      "The more generic the slower.")
2768    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2769  let hbox =
2770   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2771  let lMessage =
2772   GMisc.label
2773    ~text:
2774     "Suggestion: start with faster queries before moving to more generic ones."
2775    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2776  let notebook =
2777   GPack.notebook ~scrollable:true
2778    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2779  let _ =
2780   let page = ref 0 in
2781   let last = List.length list_of_must in
2782   List.map
2783    (function must ->
2784      incr page ;
2785      let label =
2786       GMisc.label ~text:
2787        (if !page = 1 then "More generic" else
2788          if !page = last then "More precise" else "          ") () in
2789      let expected_height = 25 * (List.length must + 2) in
2790      let height = if expected_height > 400 then 400 else expected_height in
2791      let scrolled_window =
2792       GBin.scrolled_window ~border_width:10 ~height ~width:600
2793        ~packing:(notebook#append_page ~tab_label:label#coerce) () in
2794      let clist =
2795         GList.clist ~columns:2 ~packing:scrolled_window#add
2796          ~titles:["URI" ; "Position"] ()
2797      in
2798       ignore
2799        (List.map
2800          (function (uri,position) ->
2801            let n =
2802             clist#append
2803              [uri; if position then "MainConclusion" else "Conclusion"]
2804            in
2805             clist#set_row ~selectable:false n
2806          ) must
2807        ) ;
2808       clist#columns_autosize ()
2809    ) list_of_must in
2810  let _ =
2811   let label = GMisc.label ~text:"User provided" () in
2812   let vbox =
2813    GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) () in
2814   let hbox =
2815    GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2816   let lMessage =
2817    GMisc.label
2818    ~text:"Select the constraints that must be satisfied and press OK."
2819    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2820   let expected_height = 25 * (List.length only + 2) in
2821   let height = if expected_height > 400 then 400 else expected_height in
2822   let scrolled_window =
2823    GBin.scrolled_window ~border_width:10 ~height ~width:600
2824     ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2825   let clist =
2826    GList.clist ~columns:2 ~packing:scrolled_window#add
2827     ~selection_mode:`EXTENDED
2828     ~titles:["URI" ; "Position"] ()
2829   in
2830    ignore
2831     (List.map
2832       (function (uri,position) ->
2833         let n =
2834          clist#append
2835           [uri; if position then "MainConclusion" else "Conclusion"]
2836         in
2837          clist#set_row ~selectable:true n
2838       ) only
2839     ) ;
2840    clist#columns_autosize () ;
2841    ignore
2842     (clist#connect#select_row
2843       (fun ~row ~column ~event ->
2844         user_constraints := (List.nth only row)::!user_constraints)) ;
2845    ignore
2846     (clist#connect#unselect_row
2847       (fun ~row ~column ~event ->
2848         user_constraints :=
2849          List.filter
2850           (function uri -> uri != (List.nth only row)) !user_constraints)) ;
2851  in
2852  let hbox =
2853   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2854  let okb =
2855   GButton.button ~label:"Ok"
2856    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2857  let cancelb =
2858   GButton.button ~label:"Abort"
2859    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2860  (* actions *)
2861  ignore (window#connect#destroy GMain.Main.quit) ;
2862  ignore (cancelb#connect#clicked window#destroy) ;
2863  ignore
2864   (okb#connect#clicked
2865     (function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
2866  window#set_position `CENTER ;
2867  window#show () ;
2868  GMain.Main.main () ;
2869  match !chosen with
2870     None -> raise NoChoice
2871   | Some n ->
2872      if n = List.length list_of_must then
2873       (* user provided constraints *)
2874       !user_constraints
2875      else
2876       List.nth list_of_must n
2877 ;;
2878
2879 let searchPattern () =
2880  let inputt = ((rendering_window ())#inputt : term_editor) in
2881  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2882   try
2883     let metasenv =
2884      match !ProofEngine.proof with
2885         None -> assert false
2886       | Some (_,metasenv,_,_) -> metasenv
2887     in
2888      match !ProofEngine.goal with
2889         None -> ()
2890       | Some metano ->
2891          let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
2892           let list_of_must,only = MQueryLevels.out_restr metasenv ey ty in
2893           let must = choose_must list_of_must only in
2894           let torigth_restriction (u,b) =
2895            let p =
2896             if b then
2897              "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion"
2898             else
2899              "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"
2900            in
2901             (u,p,None)
2902           in
2903           let rigth_must = List.map torigth_restriction must in
2904           let rigth_only = Some (List.map torigth_restriction only) in
2905           let result =
2906            MQueryGenerator.searchPattern
2907             (rigth_must,[],[]) (rigth_only,None,None) in
2908           let uris =
2909            List.map
2910             (function uri,_ ->
2911               wrong_xpointer_format_from_wrong_xpointer_format' uri
2912             ) result in
2913           let html =
2914            " <h1>Backward Query: </h1>" ^
2915            " <pre>" ^ get_last_query result ^ "</pre>"
2916           in
2917            output_html outputhtml html ;
2918            let uris',exc =
2919             let rec filter_out =
2920              function
2921                 [] -> [],""
2922               | uri::tl ->
2923                  let tl',exc = filter_out tl in
2924                   try
2925                    if
2926                     ProofEngine.can_apply
2927                      (term_of_cic_textual_parser_uri
2928                       (cic_textual_parser_uri_of_string uri))
2929                    then
2930                     uri::tl',exc
2931                    else
2932                     tl',exc
2933                   with
2934                    e ->
2935                     let exc' =
2936                      "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
2937                       uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
2938                     in
2939                      tl',exc'
2940             in
2941              filter_out uris
2942            in
2943             let html' =
2944              " <h1>Objects that can actually be applied: </h1> " ^
2945              String.concat "<br>" uris' ^ exc ^
2946              " <h1>Number of false matches: " ^
2947               string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
2948              " <h1>Number of good matches: " ^
2949               string_of_int (List.length uris') ^ "</h1>"
2950             in
2951              output_html outputhtml html' ;
2952              let uri' =
2953               user_uri_choice ~title:"Ambiguous input."
2954               ~msg:
2955                 "Many lemmas can be successfully applied. Please, choose one:"
2956                uris'
2957              in
2958               inputt#set_term uri' ;
2959               apply ()
2960   with
2961    e ->
2962     output_html outputhtml
2963      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2964 ;;
2965
2966 let choose_selection
2967      (mmlwidget : GMathView.math_view) (element : Gdome.element option)
2968 =
2969  let module G = Gdome in
2970   let rec aux element =
2971    if element#hasAttributeNS
2972        ~namespaceURI:helmns
2973        ~localName:(G.domString "xref")
2974    then
2975      mmlwidget#set_selection (Some element)
2976    else
2977       match element#get_parentNode with
2978          None -> assert false
2979        (*CSC: OCAML DIVERGES!
2980        | Some p -> aux (new G.element_of_node p)
2981        *)
2982        | Some p -> aux (new Gdome.element_of_node p)
2983   in
2984    match element with
2985      Some x -> aux x
2986    | None   -> mmlwidget#set_selection None
2987 ;;
2988
2989 (* STUFF TO BUILD THE GTK INTERFACE *)
2990
2991 (* Stuff for the widget settings *)
2992
2993 let export_to_postscript (output : GMathView.math_view) =
2994  let lastdir = ref (Unix.getcwd ()) in
2995   function () ->
2996    match
2997     GToolbox.select_file ~title:"Export to PostScript"
2998      ~dir:lastdir ~filename:"screenshot.ps" ()
2999    with
3000       None -> ()
3001     | Some filename ->
3002        output#export_to_postscript ~filename:filename ();
3003 ;;
3004
3005 let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
3006  button_set_kerning button_set_transparency export_to_postscript_menu_item
3007  button_t1 ()
3008 =
3009  let is_set = button_t1#active in
3010   output#set_font_manager_type
3011    (if is_set then `font_manager_t1 else `font_manager_gtk) ;
3012   if is_set then
3013    begin
3014     button_set_anti_aliasing#misc#set_sensitive true ;
3015     button_set_kerning#misc#set_sensitive true ;
3016     button_set_transparency#misc#set_sensitive true ;
3017     export_to_postscript_menu_item#misc#set_sensitive true ;
3018    end
3019   else
3020    begin
3021     button_set_anti_aliasing#misc#set_sensitive false ;
3022     button_set_kerning#misc#set_sensitive false ;
3023     button_set_transparency#misc#set_sensitive false ;
3024     export_to_postscript_menu_item#misc#set_sensitive false ;
3025    end
3026 ;;
3027
3028 let set_anti_aliasing output button_set_anti_aliasing () =
3029  output#set_anti_aliasing button_set_anti_aliasing#active
3030 ;;
3031
3032 let set_kerning output button_set_kerning () =
3033  output#set_kerning button_set_kerning#active
3034 ;;
3035
3036 let set_transparency output button_set_transparency () =
3037  output#set_transparency button_set_transparency#active
3038 ;;
3039
3040 let changefont output font_size_spinb () =
3041  output#set_font_size font_size_spinb#value_as_int
3042 ;;
3043
3044 let set_log_verbosity output log_verbosity_spinb () =
3045  output#set_log_verbosity log_verbosity_spinb#value_as_int
3046 ;;
3047
3048 class settings_window (output : GMathView.math_view) sw
3049  export_to_postscript_menu_item selection_changed_callback
3050 =
3051  let settings_window = GWindow.window ~title:"GtkMathView settings" () in
3052  let vbox =
3053   GPack.vbox ~packing:settings_window#add () in
3054  let table =
3055   GPack.table
3056    ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
3057    ~border_width:5 ~packing:vbox#add () in
3058  let button_t1 =
3059   GButton.toggle_button ~label:"activate t1 fonts"
3060    ~packing:(table#attach ~left:0 ~top:0) () in
3061  let button_set_anti_aliasing =
3062   GButton.toggle_button ~label:"set_anti_aliasing"
3063    ~packing:(table#attach ~left:0 ~top:1) () in
3064  let button_set_kerning =
3065   GButton.toggle_button ~label:"set_kerning"
3066    ~packing:(table#attach ~left:1 ~top:1) () in
3067  let button_set_transparency =
3068   GButton.toggle_button ~label:"set_transparency"
3069    ~packing:(table#attach ~left:2 ~top:1) () in
3070  let table =
3071   GPack.table
3072    ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
3073    ~border_width:5 ~packing:vbox#add () in
3074  let font_size_label =
3075   GMisc.label ~text:"font size:"
3076    ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
3077  let font_size_spinb =
3078   let sadj =
3079    GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
3080   in
3081    GEdit.spin_button
3082     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
3083  let log_verbosity_label =
3084   GMisc.label ~text:"log verbosity:"
3085    ~packing:(table#attach ~left:0 ~top:1) () in
3086  let log_verbosity_spinb =
3087   let sadj =
3088    GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
3089   in
3090    GEdit.spin_button
3091     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
3092  let hbox =
3093   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
3094  let closeb =
3095   GButton.button ~label:"Close"
3096    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
3097 object(self)
3098  method show = settings_window#show
3099  initializer
3100   button_set_anti_aliasing#misc#set_sensitive false ;
3101   button_set_kerning#misc#set_sensitive false ;
3102   button_set_transparency#misc#set_sensitive false ;
3103   (* Signals connection *)
3104   ignore(button_t1#connect#clicked
3105    (activate_t1 output button_set_anti_aliasing button_set_kerning
3106     button_set_transparency export_to_postscript_menu_item button_t1)) ;
3107   ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
3108   ignore(button_set_anti_aliasing#connect#toggled
3109    (set_anti_aliasing output button_set_anti_aliasing));
3110   ignore(button_set_kerning#connect#toggled
3111    (set_kerning output button_set_kerning)) ;
3112   ignore(button_set_transparency#connect#toggled
3113    (set_transparency output button_set_transparency)) ;
3114   ignore(log_verbosity_spinb#connect#changed
3115    (set_log_verbosity output log_verbosity_spinb)) ;
3116   ignore(closeb#connect#clicked settings_window#misc#hide)
3117 end;;
3118
3119 (* Scratch window *)
3120
3121 class scratch_window =
3122  let window =
3123   GWindow.window ~title:"MathML viewer" ~border_width:2 () in
3124  let vbox =
3125   GPack.vbox ~packing:window#add () in
3126  let hbox =
3127   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
3128  let whdb =
3129   GButton.button ~label:"Whd"
3130    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
3131  let reduceb =
3132   GButton.button ~label:"Reduce"
3133    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
3134  let simplb =
3135   GButton.button ~label:"Simpl"
3136    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
3137  let scrolled_window =
3138   GBin.scrolled_window ~border_width:10
3139    ~packing:(vbox#pack ~expand:true ~padding:5) () in
3140  let mmlwidget =
3141   GMathView.math_view
3142    ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
3143 object(self)
3144  method mmlwidget = mmlwidget
3145  method show () = window#misc#hide () ; window#show ()
3146  initializer
3147   ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
3148   ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
3149   ignore(whdb#connect#clicked (whd_in_scratch self)) ;
3150   ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
3151   ignore(simplb#connect#clicked (simpl_in_scratch self))
3152 end;;
3153
3154 class page () =
3155  let vbox1 = GPack.vbox () in
3156 object(self)
3157  val mutable proofw_ref = None
3158  val mutable compute_ref = None
3159  method proofw =
3160   Lazy.force self#compute ;
3161   match proofw_ref with
3162      None -> assert false
3163    | Some proofw -> proofw
3164  method content = vbox1
3165  method compute =
3166   match compute_ref with
3167      None -> assert false
3168    | Some compute -> compute
3169  initializer
3170   compute_ref <-
3171    Some (lazy (
3172    let scrolled_window1 =
3173     GBin.scrolled_window ~border_width:10
3174      ~packing:(vbox1#pack ~expand:true ~padding:5) () in
3175    let proofw =
3176     GMathView.math_view ~width:400 ~height:275
3177      ~packing:(scrolled_window1#add) () in
3178    let _ = proofw_ref <- Some proofw in
3179    let hbox3 =
3180     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3181    let exactb =
3182     GButton.button ~label:"Exact"
3183      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3184    let introsb =
3185     GButton.button ~label:"Intros"
3186      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3187    let applyb =
3188     GButton.button ~label:"Apply"
3189      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3190    let elimintrossimplb =
3191     GButton.button ~label:"ElimIntrosSimpl"
3192      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3193    let elimtypeb =
3194     GButton.button ~label:"ElimType"
3195      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3196    let whdb =
3197     GButton.button ~label:"Whd"
3198      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3199    let reduceb =
3200     GButton.button ~label:"Reduce"
3201      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3202    let simplb =
3203     GButton.button ~label:"Simpl"
3204      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3205    let hbox4 =
3206     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3207    let foldwhdb =
3208     GButton.button ~label:"Fold_whd"
3209      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3210    let foldreduceb =
3211     GButton.button ~label:"Fold_reduce"
3212      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3213    let foldsimplb =
3214     GButton.button ~label:"Fold_simpl"
3215      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3216    let cutb =
3217     GButton.button ~label:"Cut"
3218      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3219    let changeb =
3220     GButton.button ~label:"Change"
3221      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3222    let letinb =
3223     GButton.button ~label:"Let ... In"
3224      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3225    let ringb =
3226     GButton.button ~label:"Ring"
3227      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3228    let hbox5 =
3229     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3230    let clearbodyb =
3231     GButton.button ~label:"ClearBody"
3232      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3233    let clearb =
3234     GButton.button ~label:"Clear"
3235      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3236    let fourierb =
3237     GButton.button ~label:"Fourier"
3238      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3239    let rewritesimplb =
3240     GButton.button ~label:"RewriteSimpl ->"
3241      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3242    let rewritebacksimplb =
3243     GButton.button ~label:"RewriteSimpl <-"
3244      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3245    let replaceb =
3246     GButton.button ~label:"Replace"
3247      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3248    let hbox6 =
3249     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3250    let reflexivityb =
3251     GButton.button ~label:"Reflexivity"
3252      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3253    let symmetryb =
3254     GButton.button ~label:"Symmetry"
3255      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3256    let transitivityb =
3257     GButton.button ~label:"Transitivity"
3258      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3259    let existsb =
3260     GButton.button ~label:"Exists"
3261      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3262    let splitb =
3263     GButton.button ~label:"Split"
3264      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3265    let leftb =
3266     GButton.button ~label:"Left"
3267      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3268    let rightb =
3269     GButton.button ~label:"Right"
3270      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3271    let assumptionb =
3272     GButton.button ~label:"Assumption"
3273      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3274    let hbox7 =
3275     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3276    let generalizeb =
3277     GButton.button ~label:"Generalize"
3278      ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3279    let absurdb =
3280     GButton.button ~label:"Absurd"
3281      ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3282    let contradictionb =
3283     GButton.button ~label:"Contradiction"
3284      ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3285    let searchpatternb =
3286     GButton.button ~label:"SearchPattern_Apply"
3287      ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3288
3289    ignore(exactb#connect#clicked exact) ;
3290    ignore(applyb#connect#clicked apply) ;
3291    ignore(elimintrossimplb#connect#clicked elimintrossimpl) ;
3292    ignore(elimtypeb#connect#clicked elimtype) ;
3293    ignore(whdb#connect#clicked whd) ;
3294    ignore(reduceb#connect#clicked reduce) ;
3295    ignore(simplb#connect#clicked simpl) ;
3296    ignore(foldwhdb#connect#clicked fold_whd) ;
3297    ignore(foldreduceb#connect#clicked fold_reduce) ;
3298    ignore(foldsimplb#connect#clicked fold_simpl) ;
3299    ignore(cutb#connect#clicked cut) ;
3300    ignore(changeb#connect#clicked change) ;
3301    ignore(letinb#connect#clicked letin) ;
3302    ignore(ringb#connect#clicked ring) ;
3303    ignore(clearbodyb#connect#clicked clearbody) ;
3304    ignore(clearb#connect#clicked clear) ;
3305    ignore(fourierb#connect#clicked fourier) ;
3306    ignore(rewritesimplb#connect#clicked rewritesimpl) ;
3307    ignore(rewritebacksimplb#connect#clicked rewritebacksimpl) ;
3308    ignore(replaceb#connect#clicked replace) ;
3309    ignore(reflexivityb#connect#clicked reflexivity) ;
3310    ignore(symmetryb#connect#clicked symmetry) ;
3311    ignore(transitivityb#connect#clicked transitivity) ;
3312    ignore(existsb#connect#clicked exists) ;
3313    ignore(splitb#connect#clicked split) ;
3314    ignore(leftb#connect#clicked left) ;
3315    ignore(rightb#connect#clicked right) ;
3316    ignore(assumptionb#connect#clicked assumption) ;
3317    ignore(generalizeb#connect#clicked generalize) ;
3318    ignore(absurdb#connect#clicked absurd) ;
3319    ignore(contradictionb#connect#clicked contradiction) ;
3320    ignore(introsb#connect#clicked intros) ;
3321    ignore(searchpatternb#connect#clicked searchPattern) ;
3322    ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
3323   ))
3324 end
3325 ;;
3326
3327 class empty_page =
3328  let vbox1 = GPack.vbox () in
3329  let scrolled_window1 =
3330   GBin.scrolled_window ~border_width:10
3331    ~packing:(vbox1#pack ~expand:true ~padding:5) () in
3332  let proofw =
3333   GMathView.math_view ~width:400 ~height:275
3334    ~packing:(scrolled_window1#add) () in
3335 object(self)
3336  method proofw = (assert false : GMathView.math_view)
3337  method content = vbox1
3338  method compute = (assert false : unit)
3339 end
3340 ;;
3341
3342 let empty_page = new empty_page;;
3343
3344 class notebook =
3345 object(self)
3346  val notebook = GPack.notebook ()
3347  val pages = ref []
3348  val mutable skip_switch_page_event = false
3349  val mutable empty = true
3350  method notebook = notebook
3351  method add_page n =
3352   let new_page = new page () in
3353    empty <- false ;
3354    pages := !pages @ [n,lazy (setgoal n),new_page] ;
3355    notebook#append_page
3356     ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce)
3357     new_page#content#coerce
3358  method remove_all_pages ~skip_switch_page_event:skip =
3359   if empty then
3360    notebook#remove_page 0 (* let's remove the empty page *)
3361   else
3362    List.iter (function _ -> notebook#remove_page 0) !pages ;
3363   pages := [] ;
3364   skip_switch_page_event <- skip
3365  method set_current_page ~may_skip_switch_page_event n =
3366   let (_,_,page) = List.find (function (m,_,_) -> m=n) !pages in
3367    let new_page = notebook#page_num page#content#coerce in
3368     if may_skip_switch_page_event && new_page <> notebook#current_page then
3369      skip_switch_page_event <- true ;
3370     notebook#goto_page new_page
3371  method set_empty_page =
3372   empty <- true ;
3373   pages := [] ;
3374   notebook#append_page
3375    ~tab_label:((GMisc.label ~text:"No proof in progress" ())#coerce)
3376    empty_page#content#coerce
3377  method proofw =
3378   let (_,_,page) = List.nth !pages notebook#current_page in
3379    page#proofw
3380  initializer
3381   ignore
3382    (notebook#connect#switch_page
3383     (function i ->
3384       let skip = skip_switch_page_event in
3385        skip_switch_page_event <- false ;
3386        if not skip then
3387         try
3388          let (metano,setgoal,page) = List.nth !pages i in
3389           ProofEngine.goal := Some metano ;
3390           Lazy.force (page#compute) ;
3391           Lazy.force setgoal
3392         with _ -> ()
3393     ))
3394 end
3395 ;;
3396
3397 (* Main window *)
3398
3399 class rendering_window output (notebook : notebook) =
3400  let scratch_window = new scratch_window in
3401  let window =
3402   GWindow.window ~title:"MathML viewer" ~border_width:0
3403    ~allow_shrink:false () in
3404  let vbox_for_menu = GPack.vbox ~packing:window#add () in
3405  (* menus *)
3406  let handle_box = GBin.handle_box ~border_width:2
3407   ~packing:(vbox_for_menu#pack ~padding:0) () in
3408  let menubar = GMenu.menu_bar ~packing:handle_box#add () in
3409  let factory0 = new GMenu.factory menubar in
3410  let accel_group = factory0#accel_group in
3411  (* file menu *)
3412  let file_menu = factory0#add_submenu "File" in
3413  let factory1 = new GMenu.factory file_menu ~accel_group in
3414  let export_to_postscript_menu_item =
3415   begin
3416    let _ =
3417     factory1#add_item "New Block of (Co)Inductive Definitions..."
3418      ~key:GdkKeysyms._B ~callback:new_inductive
3419    in
3420    let _ =
3421     factory1#add_item "New Proof or Definition..." ~key:GdkKeysyms._N
3422      ~callback:new_proof
3423    in
3424    let reopen_menu_item =
3425     factory1#add_item "Reopen a Finished Proof..." ~key:GdkKeysyms._R
3426      ~callback:open_
3427    in
3428    let qed_menu_item =
3429     factory1#add_item "Qed" ~key:GdkKeysyms._E ~callback:qed in
3430    ignore (factory1#add_separator ()) ;
3431    ignore
3432     (factory1#add_item "Load Unfinished Proof..." ~key:GdkKeysyms._L
3433       ~callback:load) ;
3434    let save_menu_item =
3435     factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S ~callback:save
3436    in
3437    ignore
3438     (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b);
3439    ignore (!save_set_sensitive false);
3440    ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b);
3441    ignore (!qed_set_sensitive false);
3442    ignore (factory1#add_separator ()) ;
3443    let export_to_postscript_menu_item =
3444     factory1#add_item "Export to PostScript..."
3445      ~callback:(export_to_postscript output) in
3446    ignore (factory1#add_separator ()) ;
3447    ignore
3448     (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) ;
3449    export_to_postscript_menu_item
3450   end in
3451  (* edit menu *)
3452  let edit_menu = factory0#add_submenu "Edit Current Proof" in
3453  let factory2 = new GMenu.factory edit_menu ~accel_group in
3454  let focus_and_proveit_set_sensitive = ref (function _ -> assert false) in
3455  let proveit_menu_item =
3456   factory2#add_item "Prove It" ~key:GdkKeysyms._I
3457    ~callback:(function () -> proveit ();!focus_and_proveit_set_sensitive false)
3458  in
3459  let focus_menu_item =
3460   factory2#add_item "Focus" ~key:GdkKeysyms._F
3461    ~callback:(function () -> focus () ; !focus_and_proveit_set_sensitive false)
3462  in
3463  let _ =
3464   focus_and_proveit_set_sensitive :=
3465    function b ->
3466     proveit_menu_item#misc#set_sensitive b ;
3467     focus_menu_item#misc#set_sensitive b
3468  in
3469  let _ = !focus_and_proveit_set_sensitive false in
3470  (* edit term menu *)
3471  let edit_term_menu = factory0#add_submenu "Edit Term" in
3472  let factory5 = new GMenu.factory edit_term_menu ~accel_group in
3473  let check_menu_item =
3474   factory5#add_item "Check Term" ~key:GdkKeysyms._C
3475    ~callback:(check scratch_window) in
3476  let _ = check_menu_item#misc#set_sensitive false in
3477  (* search menu *)
3478  let settings_menu = factory0#add_submenu "Search" in
3479  let factory4 = new GMenu.factory settings_menu ~accel_group in
3480  let _ =
3481   factory4#add_item "Locate..." ~key:GdkKeysyms._T
3482    ~callback:locate in
3483  let searchPattern_menu_item =
3484   factory4#add_item "SearchPattern..." ~key:GdkKeysyms._D
3485    ~callback:completeSearchPattern in
3486  let _ = searchPattern_menu_item#misc#set_sensitive false in
3487  let show_menu_item =
3488   factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show
3489  in
3490  let insert_query_item =
3491   factory4#add_item "Insert Query (Experts Only)..." ~key:GdkKeysyms._U
3492    ~callback:insertQuery in
3493  (* settings menu *)
3494  let settings_menu = factory0#add_submenu "Settings" in
3495  let factory3 = new GMenu.factory settings_menu ~accel_group in
3496  let _ =
3497   factory3#add_item "Edit Aliases" ~key:GdkKeysyms._A
3498    ~callback:edit_aliases in
3499  let _ = factory3#add_separator () in
3500  let _ =
3501   factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P
3502    ~callback:(function _ -> (settings_window ())#show ()) in
3503  (* accel group *)
3504  let _ = window#add_accel_group accel_group in
3505  (* end of menus *)
3506  let hbox0 =
3507   GPack.hbox
3508    ~packing:(vbox_for_menu#pack ~expand:true ~fill:true ~padding:5) () in
3509  let vbox =
3510   GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
3511  let scrolled_window0 =
3512   GBin.scrolled_window ~border_width:10
3513    ~packing:(vbox#pack ~expand:true ~padding:5) () in
3514  let _ = scrolled_window0#add output#coerce in
3515  let frame =
3516   GBin.frame ~label:"Insert Term"
3517    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
3518  let scrolled_window1 =
3519   GBin.scrolled_window ~border_width:5
3520    ~packing:frame#add () in
3521  let inputt =
3522   new term_editor ~width:400 ~height:100 ~packing:scrolled_window1#add ()
3523    ~isnotempty_callback:
3524     (function b ->
3525       check_menu_item#misc#set_sensitive b ;
3526       searchPattern_menu_item#misc#set_sensitive b) in
3527  let vboxl =
3528   GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
3529  let _ =
3530   vboxl#pack ~expand:true ~fill:true ~padding:5 notebook#notebook#coerce in
3531  let frame =
3532   GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
3533  in
3534  let outputhtml =
3535   GHtml.xmhtml
3536    ~source:"<html><body bgColor=\"white\"></body></html>"
3537    ~width:400 ~height: 100
3538    ~border_width:20
3539    ~packing:frame#add
3540    ~show:true () in
3541 object
3542  method outputhtml = outputhtml
3543  method inputt = inputt
3544  method output = (output : GMathView.math_view)
3545  method notebook = notebook
3546  method show = window#show
3547  initializer
3548   notebook#set_empty_page ;
3549   export_to_postscript_menu_item#misc#set_sensitive false ;
3550   check_term := (check_term_in_scratch scratch_window) ;
3551
3552   (* signal handlers here *)
3553   ignore(output#connect#selection_changed
3554    (function elem ->
3555      choose_selection output elem ;
3556      !focus_and_proveit_set_sensitive true
3557    )) ;
3558   ignore (output#connect#clicked (show_in_show_window_callback output)) ;
3559   let settings_window = new settings_window output scrolled_window0
3560    export_to_postscript_menu_item (choose_selection output) in
3561   set_settings_window settings_window ;
3562   set_outputhtml outputhtml ;
3563   ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
3564   Logger.log_callback :=
3565    (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
3566 end;;
3567
3568 (* MAIN *)
3569
3570 let initialize_everything () =
3571  let module U = Unix in
3572   let output = GMathView.math_view ~width:350 ~height:280 () in
3573   let notebook = new notebook in
3574    let rendering_window' = new rendering_window output notebook in
3575     set_rendering_window rendering_window' ;
3576     mml_of_cic_term_ref := mml_of_cic_term ;
3577     rendering_window'#show () ;
3578     GMain.Main.main ()
3579 ;;
3580
3581 let _ =
3582  if !usedb then
3583   begin
3584    Mqint.set_database Mqint.postgres_db ;
3585    Mqint.init postgresqlconnectionstring ;
3586   end ;
3587  ignore (GtkMain.Main.init ()) ;
3588  initialize_everything () ;
3589  if !usedb then Mqint.close ();
3590 ;;