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 (* TASSI *)
  64 let prooffile = "/home/tassi/miohelm/tmp/currentproof";;
  65 let prooffiletype = "/home/tassi/miohelm/tmp/currentprooftype";;
  66
  67 (*
  68 let prooffile = "/public/sacerdot/currentproof";;
  69 let prooffiletype = "/public/sacerdot/currentprooftype";;
  70 *)
  71
  72
  73 (*CSC: the getter should handle the innertypes, not the FS *)
  74
  75 (* TASSI *)
  76 let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";;
  77 let constanttypefile = "/home/tassi/miohelm/tmp/constanttype";;
  78
  79 (*
  80 let innertypesfile = "/public/sacerdot/innertypes";;
  81 let constanttypefile = "/public/sacerdot/constanttype";;
  82 *)
  83
  84 let empty_id_to_uris = ([],function _ -> None);;
  85
  86
  87 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
  88
  89 let htmlheader_and_content = ref htmlheader;;
  90
  91 let current_cic_infos = ref None;;
  92 let current_goal_infos = ref None;;
  93 let current_scratch_infos = ref None;;
  94
  95 let id_to_uris = ref empty_id_to_uris;;
  96
  97 let check_term = ref (fun _ _ _ -> assert false);;
  98 let mml_of_cic_term_ref = ref (fun _ _ -> assert false);;
  99
 100 exception RenderingWindowsNotInitialized;;
 101
 102 let set_rendering_window,rendering_window =
 103  let rendering_window_ref = ref None in
 104   (function rw -> rendering_window_ref := Some rw),
 105   (function () ->
 106     match !rendering_window_ref with
 107        None -> raise RenderingWindowsNotInitialized
 108      | Some rw -> rw
 109   )
 110 ;;
 111
 112 exception SettingsWindowsNotInitialized;;
 113
 114 let set_settings_window,settings_window =
 115  let settings_window_ref = ref None in
 116   (function rw -> settings_window_ref := Some rw),
 117   (function () ->
 118     match !settings_window_ref with
 119        None -> raise SettingsWindowsNotInitialized
 120      | Some rw -> rw
 121   )
 122 ;;
 123
 124 exception OutputHtmlNotInitialized;;
 125
 126 let set_outputhtml,outputhtml =
 127  let outputhtml_ref = ref None in
 128   (function rw -> outputhtml_ref := Some rw),
 129   (function () ->
 130     match !outputhtml_ref with
 131        None -> raise OutputHtmlNotInitialized
 132      | Some outputhtml -> outputhtml
 133   )
 134 ;;
 135
 136 exception QedSetSensitiveNotInitialized;;
 137 let qed_set_sensitive =
 138  ref (function _ -> raise QedSetSensitiveNotInitialized)
 139 ;;
 140
 141 exception SaveSetSensitiveNotInitialized;;
 142 let save_set_sensitive =
 143  ref (function _ -> raise SaveSetSensitiveNotInitialized)
 144 ;;
 145
 146 (* COMMAND LINE OPTIONS *)
 147
 148 let usedb = ref true
 149
 150 let argspec =
 151   [
 152     "-nodb", Arg.Clear usedb, "disable use of MathQL DB"
 153   ]
 154 in
 155 Arg.parse argspec ignore ""
 156
 157 (* A WIDGET TO ENTER CIC TERMS *)
 158
 159 class term_editor ?packing ?width ?height ?isnotempty_callback () =
 160  let input = GEdit.text ~editable:true ?width ?height ?packing () in
 161  let _ =
 162   match isnotempty_callback with
 163      None -> ()
 164    | Some callback ->
 165       ignore(input#connect#changed (function () -> callback (input#length > 0)))
 166  in
 167 object(self)
 168  method coerce = input#coerce
 169  method reset =
 170   input#delete_text 0 input#length
 171  (* CSC: txt is now a string, but should be of type Cic.term *)
 172  method set_term txt =
 173   self#reset ;
 174   ignore ((input#insert_text txt) ~pos:0)
 175  (* CSC: this method should disappear *)
 176  method get_as_string =
 177   input#get_chars 0 input#length
 178  method get_term ~context ~metasenv =
 179   let lexbuf = Lexing.from_string (input#get_chars 0 input#length) in
 180    CicTextualParserContext.main ~context ~metasenv CicTextualLexer.token lexbuf
 181 end
 182 ;;
 183
 184 (* MISC FUNCTIONS *)
 185
 186 exception IllFormedUri of string;;
 187
 188 let cic_textual_parser_uri_of_string uri' =
 189  try
 190   (* Constant *)
 191   if String.sub uri' (String.length uri' - 4) 4 = ".con" then
 192    CicTextualParser0.ConUri (UriManager.uri_of_string uri')
 193   else
 194    if String.sub uri' (String.length uri' - 4) 4 = ".var" then
 195     CicTextualParser0.VarUri (UriManager.uri_of_string uri')
 196    else
 197     (try
 198       (* Inductive Type *)
 199       let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
 200        CicTextualParser0.IndTyUri (uri'',typeno)
 201      with
 202       _ ->
 203        (* Constructor of an Inductive Type *)
 204        let uri'',typeno,consno =
 205         CicTextualLexer.indconuri_of_uri uri'
 206        in
 207         CicTextualParser0.IndConUri (uri'',typeno,consno)
 208     )
 209  with
 210   _ -> raise (IllFormedUri uri')
 211 ;;
 212
 213 let term_of_cic_textual_parser_uri uri =
 214  let module C = Cic in
 215  let module CTP = CicTextualParser0 in
 216   match uri with
 217      CTP.ConUri uri -> C.Const (uri,[])
 218    | CTP.VarUri uri -> C.Var (uri,[])
 219    | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[])
 220    | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[])
 221 ;;
 222
 223 let string_of_cic_textual_parser_uri uri =
 224  let module C = Cic in
 225  let module CTP = CicTextualParser0 in
 226   let uri' =
 227    match uri with
 228       CTP.ConUri uri -> UriManager.string_of_uri uri
 229     | CTP.VarUri uri -> UriManager.string_of_uri uri
 230     | CTP.IndTyUri (uri,tyno) ->
 231        UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1)
 232     | CTP.IndConUri (uri,tyno,consno) ->
 233        UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^
 234         string_of_int consno
 235   in
 236    (* 4 = String.length "cic:" *)
 237    String.sub uri' 4 (String.length uri' - 4)
 238 ;;
 239
 240 let output_html outputhtml msg =
 241  htmlheader_and_content := !htmlheader_and_content ^ msg ;
 242  outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
 243  outputhtml#set_topline (-1)
 244 ;;
 245
 246 (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *)
 247
 248 (* Check window *)
 249
 250 let check_window outputhtml uris =
 251  let window =
 252   GWindow.window
 253    ~width:800 ~modal:true ~title:"Check" ~border_width:2 () in
 254  let notebook =
 255   GPack.notebook ~scrollable:true ~packing:window#add () in
 256  window#show () ;
 257  let render_terms =
 258   List.map
 259    (function uri ->
 260      let scrolled_window =
 261       GBin.scrolled_window ~border_width:10
 262        ~packing:
 263          (notebook#append_page ~tab_label:((GMisc.label ~text:uri ())#coerce))
 264        ()
 265      in
 266       lazy
 267        (let mmlwidget =
 268          GMathView.math_view
 269           ~packing:scrolled_window#add ~width:400 ~height:280 () in
 270         let expr =
 271          let term =
 272           term_of_cic_textual_parser_uri (cic_textual_parser_uri_of_string uri)
 273          in
 274           (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term))
 275         in
 276          try
 277           let mml = !mml_of_cic_term_ref 111 expr in
 278 prerr_endline ("### " ^ CicPp.ppterm expr) ;
 279            mmlwidget#load_tree ~dom:mml
 280          with
 281           e ->
 282            output_html outputhtml
 283             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 284        )
 285    ) uris
 286  in
 287   ignore
 288    (notebook#connect#switch_page
 289      (function i -> Lazy.force (List.nth render_terms i)))
 290 ;;
 291
 292 exception NoChoice;;
 293
 294 let
 295  interactive_user_uri_choice ~selection_mode ?(ok="Ok") ~title ~msg uris
 296 =
 297  let choices = ref [] in
 298  let chosen = ref false in
 299  let window =
 300   GWindow.dialog ~modal:true ~title ~width:600 () in
 301  let lMessage =
 302   GMisc.label ~text:msg
 303    ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
 304  let scrolled_window =
 305   GBin.scrolled_window ~border_width:10
 306    ~packing:(window#vbox#pack ~expand:true ~fill:true ~padding:5) () in
 307  let clist =
 308   let expected_height = 18 * List.length uris in
 309    let height = if expected_height > 400 then 400 else expected_height in
 310     GList.clist ~columns:1 ~packing:scrolled_window#add
 311      ~height ~selection_mode () in
 312  let _ = List.map (function x -> clist#append [x]) uris in
 313  let hbox2 =
 314   GPack.hbox ~border_width:0
 315    ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
 316  let explain_label =
 317   GMisc.label ~text:"None of the above. Try this one:"
 318    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
 319  let manual_input =
 320   GEdit.entry ~editable:true
 321    ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
 322  let hbox =
 323   GPack.hbox ~border_width:0 ~packing:window#action_area#add () in
 324  let okb =
 325   GButton.button ~label:ok
 326    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 327  let _ = okb#misc#set_sensitive false in
 328  let checkb =
 329   GButton.button ~label:"Check"
 330    ~packing:(hbox#pack ~padding:5) () in
 331  let _ = checkb#misc#set_sensitive false in
 332  let cancelb =
 333   GButton.button ~label:"Abort"
 334    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 335  (* actions *)
 336  let check_callback () =
 337   assert (List.length !choices > 0) ;
 338   check_window (outputhtml ()) !choices
 339  in
 340   ignore (window#connect#destroy GMain.Main.quit) ;
 341   ignore (cancelb#connect#clicked window#destroy) ;
 342   ignore
 343    (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
 344   ignore (checkb#connect#clicked check_callback) ;
 345   ignore
 346    (clist#connect#select_row
 347      (fun ~row ~column ~event ->
 348        checkb#misc#set_sensitive true ;
 349        okb#misc#set_sensitive true ;
 350        choices := (List.nth uris row)::!choices)) ;
 351   ignore
 352    (clist#connect#unselect_row
 353      (fun ~row ~column ~event ->
 354        choices :=
 355         List.filter (function uri -> uri != (List.nth uris row)) !choices)) ;
 356   ignore
 357    (manual_input#connect#changed
 358      (fun _ ->
 359        if manual_input#text = "" then
 360         begin
 361          choices := [] ;
 362          checkb#misc#set_sensitive false ;
 363          okb#misc#set_sensitive false ;
 364          clist#misc#set_sensitive true
 365         end
 366        else
 367         begin
 368          choices := [manual_input#text] ;
 369          clist#unselect_all () ;
 370          checkb#misc#set_sensitive true ;
 371          okb#misc#set_sensitive true ;
 372          clist#misc#set_sensitive false
 373         end));
 374   window#set_position `CENTER ;
 375   window#show () ;
 376   GMain.Main.main () ;
 377   if !chosen && List.length !choices > 0 then
 378    !choices
 379   else
 380    raise NoChoice
 381 ;;
 382
 383 let interactive_interpretation_choice interpretations =
 384  let chosen = ref None in
 385  let window =
 386   GWindow.window
 387    ~modal:true ~title:"Ambiguous well-typed input." ~border_width:2 () in
 388  let vbox = GPack.vbox ~packing:window#add () in
 389  let lMessage =
 390   GMisc.label
 391    ~text:
 392     ("Ambiguous input since there are many well-typed interpretations." ^
 393      " Please, choose one of them.")
 394    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 395  let notebook =
 396   GPack.notebook ~scrollable:true
 397    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
 398  let _ =
 399   List.map
 400    (function interpretation ->
 401      let clist =
 402       let expected_height = 18 * List.length interpretation in
 403        let height = if expected_height > 400 then 400 else expected_height in
 404         GList.clist ~columns:2 ~packing:notebook#append_page ~height
 405          ~titles:["id" ; "URI"] ()
 406      in
 407       ignore
 408        (List.map
 409          (function (id,uri) ->
 410            let n = clist#append [id;uri] in
 411             clist#set_row ~selectable:false n
 412          ) interpretation
 413        ) ;
 414       clist#columns_autosize ()
 415    ) interpretations in
 416  let hbox =
 417   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 418  let okb =
 419   GButton.button ~label:"Ok"
 420    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 421  let cancelb =
 422   GButton.button ~label:"Abort"
 423    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 424  (* actions *)
 425  ignore (window#connect#destroy GMain.Main.quit) ;
 426  ignore (cancelb#connect#clicked window#destroy) ;
 427  ignore
 428   (okb#connect#clicked
 429     (function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
 430  window#set_position `CENTER ;
 431  window#show () ;
 432  GMain.Main.main () ;
 433  match !chosen with
 434     None -> raise NoChoice
 435   | Some n -> n
 436 ;;
 437
 438
 439 (* MISC FUNCTIONS *)
 440
 441 (* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
 442 let get_last_query =
 443  let query = ref "" in
 444   MQueryGenerator.set_confirm_query
 445    (function q -> query := MQueryUtil.text_of_query q ; true) ;
 446   function result -> !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
 447 ;;
 448
 449 let domImpl = Gdome.domImplementation ();;
 450
 451 let parseStyle name =
 452  let style =
 453   domImpl#createDocumentFromURI
 454 (*
 455    ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None
 456 *)
 457    ~uri:("styles/" ^ name) ()
 458  in
 459   Gdome_xslt.processStylesheet style
 460 ;;
 461
 462 let d_c = parseStyle "drop_coercions.xsl";;
 463 let tc1 = parseStyle "objtheorycontent.xsl";;
 464 let hc2 = parseStyle "content_to_html.xsl";;
 465 let l   = parseStyle "link.xsl";;
 466
 467 let c1 = parseStyle "rootcontent.xsl";;
 468 let g  = parseStyle "genmmlid.xsl";;
 469 let c2 = parseStyle "annotatedpres.xsl";;
 470
 471
 472 let getterURL = Configuration.getter_url;;
 473 let processorURL = Configuration.processor_url;;
 474
 475 let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
 476 let mml_args ~explode_all =
 477  ("explodeall",(if explode_all then "true()" else "false()"))::
 478   ["processorURL", "'" ^ processorURL ^ "'" ;
 479    "getterURL", "'" ^ getterURL ^ "'" ;
 480    "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
 481    "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
 482    "UNICODEvsSYMBOL", "'symbol'" ;
 483    "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
 484    "encoding", "'iso-8859-1'" ;
 485    "media-type", "'text/html'" ;
 486    "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
 487    "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
 488    "naturalLanguage", "'yes'" ;
 489    "annotations", "'no'" ;
 490    "URLs_or_URIs", "'URIs'" ;
 491    "topurl", "'http://phd.cs.unibo.it/helm'" ;
 492    "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
 493 ;;
 494
 495 let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
 496 let sequent_args =
 497  ["processorURL", "'" ^ processorURL ^ "'" ;
 498   "getterURL", "'" ^ getterURL ^ "'" ;
 499   "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
 500   "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
 501   "UNICODEvsSYMBOL", "'symbol'" ;
 502   "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
 503   "encoding", "'iso-8859-1'" ;
 504   "media-type", "'text/html'" ;
 505   "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
 506   "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
 507   "naturalLanguage", "'no'" ;
 508   "annotations", "'no'" ;
 509   "explodeall", "true()" ;
 510   "URLs_or_URIs", "'URIs'" ;
 511   "topurl", "'http://phd.cs.unibo.it/helm'" ;
 512   "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
 513 ;;
 514
 515 let parse_file filename =
 516  let inch = open_in filename in
 517   let rec read_lines () =
 518    try
 519     let line = input_line inch in
 520      line ^ read_lines ()
 521    with
 522     End_of_file -> ""
 523   in
 524    read_lines ()
 525 ;;
 526
 527 let applyStylesheets input styles args =
 528  List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
 529   input styles
 530 ;;
 531
 532 let
 533  mml_of_cic_object ~explode_all uri annobj ids_to_inner_sorts ids_to_inner_types
 534 =
 535 (*CSC: ????????????????? *)
 536  let xml, bodyxml =
 537   Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:true
 538    annobj
 539  in
 540  let xmlinnertypes =
 541   Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
 542    ~ask_dtd_to_the_getter:true
 543  in
 544   let input =
 545    match bodyxml with
 546       None -> Xml2Gdome.document_of_xml domImpl xml
 547     | Some bodyxml' ->
 548        Xml.pp xml (Some constanttypefile) ;
 549        Xml2Gdome.document_of_xml domImpl bodyxml'
 550   in
 551 (*CSC: We save the innertypes to disk so that we can retrieve them in the  *)
 552 (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
 553 (*CSC: local.                                                              *)
 554    Xml.pp xmlinnertypes (Some innertypesfile) ;
 555    let output = applyStylesheets input mml_styles (mml_args ~explode_all) in
 556     output
 557 ;;
 558
 559 let
 560  save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname
 561 =
 562  let name =
 563   let struri = UriManager.string_of_uri uri in
 564   let idx = (String.rindex struri '/') + 1 in
 565    String.sub struri idx (String.length struri - idx)
 566  in
 567   let path = pathname ^ "/" ^ name in
 568   let xml, bodyxml =
 569    Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false
 570     annobj
 571   in
 572   let xmlinnertypes =
 573    Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
 574     ~ask_dtd_to_the_getter:false
 575   in
 576    (* innertypes *)
 577    let innertypesuri = UriManager.innertypesuri_of_uri uri in
 578     Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ;
 579     Getter.register innertypesuri
 580      (Configuration.annotations_url ^
 581        Str.replace_first (Str.regexp "^cic:") ""
 582         (UriManager.string_of_uri innertypesuri) ^ ".xml"
 583      ) ;
 584     (* constant type / variable / mutual inductive types definition *)
 585     Xml.pp ~quiet:true xml (Some (path ^ ".xml")) ;
 586     Getter.register uri
 587      (Configuration.annotations_url ^
 588        Str.replace_first (Str.regexp "^cic:") ""
 589         (UriManager.string_of_uri uri) ^ ".xml"
 590      ) ;
 591     match bodyxml with
 592        None -> ()
 593      | Some bodyxml' ->
 594         (* constant body *)
 595         let bodyuri =
 596          match UriManager.bodyuri_of_uri uri with
 597             None -> assert false
 598           | Some bodyuri -> bodyuri
 599         in
 600          Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ;
 601          Getter.register bodyuri
 602           (Configuration.annotations_url ^
 603             Str.replace_first (Str.regexp "^cic:") ""
 604              (UriManager.string_of_uri bodyuri) ^ ".xml"
 605           )
 606 ;;
 607
 608
 609 (* CALLBACKS *)
 610
 611 exception RefreshSequentException of exn;;
 612 exception RefreshProofException of exn;;
 613
 614 let refresh_proof (output : GMathView.math_view) =
 615  try
 616   let uri,currentproof =
 617    match !ProofEngine.proof with
 618       None -> assert false
 619     | Some (uri,metasenv,bo,ty) ->
 620        !qed_set_sensitive (List.length metasenv = 0) ;
 621        (*CSC: Wrong: [] is just plainly wrong *)
 622        uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
 623   in
 624    let
 625     (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
 626      ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
 627    =
 628     Cic2acic.acic_object_of_cic_object currentproof
 629    in
 630     let mml =
 631      mml_of_cic_object ~explode_all:true uri acic ids_to_inner_sorts
 632       ids_to_inner_types
 633     in
 634      output#load_tree mml ;
 635      current_cic_infos :=
 636       Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses)
 637  with
 638   e ->
 639  match !ProofEngine.proof with
 640     None -> assert false
 641   | Some (uri,metasenv,bo,ty) ->
 642 prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
 643    raise (RefreshProofException e)
 644 ;;
 645
 646 let refresh_sequent ?(empty_notebook=true) notebook =
 647  try
 648   match !ProofEngine.goal with
 649      None ->
 650       if empty_notebook then
 651        begin
 652         notebook#remove_all_pages ~skip_switch_page_event:false ;
 653         notebook#set_empty_page
 654        end
 655       else
 656        notebook#proofw#unload
 657    | Some metano ->
 658       let metasenv =
 659        match !ProofEngine.proof with
 660           None -> assert false
 661         | Some (_,metasenv,_,_) -> metasenv
 662       in
 663       let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
 664        let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
 665         SequentPp.XmlPp.print_sequent metasenv currentsequent
 666        in
 667         let regenerate_notebook () =
 668          let skip_switch_page_event =
 669           match metasenv with
 670              (m,_,_)::_ when m = metano -> false
 671            | _ -> true
 672          in
 673           notebook#remove_all_pages ~skip_switch_page_event ;
 674           List.iter (function (m,_,_) -> notebook#add_page m) metasenv ;
 675         in
 676           if empty_notebook then
 677            begin
 678             regenerate_notebook () ;
 679             notebook#set_current_page ~may_skip_switch_page_event:false metano
 680            end
 681           else
 682            begin
 683             let sequent_doc = Xml2Gdome.document_of_xml domImpl sequent_gdome in
 684             let sequent_mml =
 685              applyStylesheets sequent_doc sequent_styles sequent_args
 686             in
 687              notebook#set_current_page ~may_skip_switch_page_event:true metano;
 688              notebook#proofw#load_tree ~dom:sequent_mml
 689            end ;
 690           current_goal_infos :=
 691            Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
 692  with
 693   e ->
 694 let metano =
 695   match !ProofEngine.goal with
 696      None -> assert false
 697    | Some m -> m
 698 in
 699 let metasenv =
 700  match !ProofEngine.proof with
 701     None -> assert false
 702   | Some (_,metasenv,_,_) -> metasenv
 703 in
 704 try
 705 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
 706 prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
 707    raise (RefreshSequentException e)
 708 with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unkown."); raise (RefreshSequentException e)
 709 ;;
 710
 711 (*
 712 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
 713  ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ;
 714 *)
 715
 716 let mml_of_cic_term metano term =
 717  let metasenv =
 718   match !ProofEngine.proof with
 719      None -> []
 720    | Some (_,metasenv,_,_) -> metasenv
 721  in
 722  let context =
 723   match !ProofEngine.goal with
 724      None -> []
 725    | Some metano ->
 726       let (_,canonical_context,_) =
 727        List.find (function (m,_,_) -> m=metano) metasenv
 728       in
 729        canonical_context
 730  in
 731    let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
 732     SequentPp.XmlPp.print_sequent metasenv (metano,context,term)
 733    in
 734     let sequent_doc =
 735      Xml2Gdome.document_of_xml domImpl sequent_gdome
 736     in
 737      let res =
 738       applyStylesheets sequent_doc sequent_styles sequent_args ;
 739      in
 740       current_scratch_infos :=
 741        Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ;
 742       res
 743 ;;
 744
 745 exception OpenConjecturesStillThere;;
 746 exception WrongProof;;
 747
 748 let pathname_of_annuri uristring =
 749  Configuration.annotations_dir ^
 750   Str.replace_first (Str.regexp "^cic:") "" uristring
 751 ;;
 752
 753 let make_dirs dirpath =
 754  ignore (Unix.system ("mkdir -p " ^ dirpath))
 755 ;;
 756
 757 let qed () =
 758  match !ProofEngine.proof with
 759     None -> assert false
 760   | Some (uri,[],bo,ty) ->
 761      if
 762       CicReduction.are_convertible []
 763        (CicTypeChecker.type_of_aux' [] [] bo) ty
 764      then
 765       begin
 766        (*CSC: Wrong: [] is just plainly wrong *)
 767        let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in
 768         let
 769          (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
 770           ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
 771         =
 772          Cic2acic.acic_object_of_cic_object proof
 773         in
 774          let mml =
 775           mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts
 776            ids_to_inner_types
 777          in
 778           ((rendering_window ())#output : GMathView.math_view)#load_tree mml ;
 779           !qed_set_sensitive false ;
 780           (* let's save the theorem and register it to the getter *)
 781           let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
 782           make_dirs pathname ;
 783           save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
 784            pathname ;
 785           current_cic_infos :=
 786            Some
 787             (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
 788              ids_to_hypotheses)
 789       end
 790      else
 791       raise WrongProof
 792   | _ -> raise OpenConjecturesStillThere
 793 ;;
 794
 795 let save () =
 796  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
 797   match !ProofEngine.proof with
 798      None -> assert false
 799    | Some (uri, metasenv, bo, ty) ->
 800       let currentproof =
 801        (*CSC: Wrong: [] is just plainly wrong *)
 802        Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
 803       in
 804        let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
 805         Cic2acic.acic_object_of_cic_object currentproof
 806        in
 807         let xml, bodyxml =
 808          match
 809           Cic2Xml.print_object uri ~ids_to_inner_sorts
 810            ~ask_dtd_to_the_getter:true acurrentproof
 811          with
 812             xml,Some bodyxml -> xml,bodyxml
 813           | _,None -> assert false
 814         in
 815          Xml.pp ~quiet:true xml (Some prooffiletype) ;
 816          output_html outputhtml
 817           ("<h1 color=\"Green\">Current proof type saved to " ^
 818            prooffiletype ^ "</h1>") ;
 819          Xml.pp ~quiet:true bodyxml (Some prooffile) ;
 820          output_html outputhtml
 821           ("<h1 color=\"Green\">Current proof body saved to " ^
 822            prooffile ^ "</h1>")
 823 ;;
 824
 825 (* Used to typecheck the loaded proofs *)
 826 let typecheck_loaded_proof metasenv bo ty =
 827  let module T = CicTypeChecker in
 828   ignore (
 829    List.fold_left
 830     (fun metasenv ((_,context,ty) as conj) ->
 831       ignore (T.type_of_aux' metasenv context ty) ;
 832       metasenv @ [conj]
 833     ) [] metasenv) ;
 834   ignore (T.type_of_aux' metasenv [] ty) ;
 835   ignore (T.type_of_aux' metasenv [] bo)
 836 ;;
 837
 838 let load () =
 839  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
 840  let output = ((rendering_window ())#output : GMathView.math_view) in
 841  let notebook = (rendering_window ())#notebook in
 842   try
 843    match
 844     GToolbox.input_string ~title:"Load Unfinished Proof" ~text:"/dummy.con"
 845      "Choose an URI:"
 846    with
 847       None -> raise NoChoice
 848     | Some uri0 ->
 849        let uri = UriManager.uri_of_string ("cic:" ^ uri0) in
 850         match CicParser.obj_of_xml prooffiletype (Some prooffile) with
 851            Cic.CurrentProof (_,metasenv,bo,ty,_) ->
 852             typecheck_loaded_proof metasenv bo ty ;
 853             ProofEngine.proof :=
 854              Some (uri, metasenv, bo, ty) ;
 855             ProofEngine.goal :=
 856              (match metasenv with
 857                  [] -> None
 858                | (metano,_,_)::_ -> Some metano
 859              ) ;
 860             refresh_proof output ;
 861             refresh_sequent notebook ;
 862              output_html outputhtml
 863               ("<h1 color=\"Green\">Current proof type loaded from " ^
 864                 prooffiletype ^ "</h1>") ;
 865              output_html outputhtml
 866               ("<h1 color=\"Green\">Current proof body loaded from " ^
 867                 prooffile ^ "</h1>") ;
 868             !save_set_sensitive true
 869          | _ -> assert false
 870   with
 871      RefreshSequentException e ->
 872       output_html outputhtml
 873        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 874         "sequent: " ^ Printexc.to_string e ^ "</h1>")
 875    | RefreshProofException e ->
 876       output_html outputhtml
 877        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 878         "proof: " ^ Printexc.to_string e ^ "</h1>")
 879    | e ->
 880       output_html outputhtml
 881        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 882 ;;
 883
 884 let edit_aliases () =
 885  let chosen = ref false in
 886  let window =
 887   GWindow.window
 888    ~width:400 ~modal:true ~title:"Edit Aliases..." ~border_width:2 () in
 889  let vbox =
 890   GPack.vbox ~border_width:0 ~packing:window#add () in
 891  let scrolled_window =
 892   GBin.scrolled_window ~border_width:10
 893    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
 894  let input = GEdit.text ~editable:true ~width:400 ~height:100
 895    ~packing:scrolled_window#add () in
 896  let hbox =
 897   GPack.hbox ~border_width:0
 898    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 899  let okb =
 900   GButton.button ~label:"Ok"
 901    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 902  let cancelb =
 903   GButton.button ~label:"Cancel"
 904    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 905  ignore (window#connect#destroy GMain.Main.quit) ;
 906  ignore (cancelb#connect#clicked window#destroy) ;
 907  ignore
 908   (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
 909  let dom,resolve_id = !id_to_uris in
 910   ignore
 911    (input#insert_text ~pos:0
 912     (String.concat "\n"
 913       (List.map
 914         (function v ->
 915           let uri =
 916            match resolve_id v with
 917               None -> assert false
 918             | Some uri -> uri
 919           in
 920            "alias " ^ v ^ " " ^
 921              (string_of_cic_textual_parser_uri uri)
 922         ) dom))) ;
 923   window#show () ;
 924   GMain.Main.main () ;
 925   if !chosen then
 926    let dom,resolve_id =
 927     let inputtext = input#get_chars 0 input#length in
 928     let regexpr =
 929      let alfa = "[a-zA-Z_-]" in
 930      let digit = "[0-9]" in
 931      let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in
 932      let blanks = "\( \|\t\|\n\)+" in
 933      let nonblanks = "[^ \t\n]+" in
 934      let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *)
 935       Str.regexp
 936        ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)")
 937     in
 938      let rec aux n =
 939       try
 940        let n' = Str.search_forward regexpr inputtext n in
 941         let id = Str.matched_group 2 inputtext in
 942         let uri =
 943          cic_textual_parser_uri_of_string
 944           ("cic:" ^ (Str.matched_group 5 inputtext))
 945         in
 946          let dom,resolve_id = aux (n' + 1) in
 947           if List.mem id dom then
 948            dom,resolve_id
 949           else
 950            id::dom,
 951             (function id' -> if id = id' then Some uri else resolve_id id')
 952       with
 953        Not_found -> empty_id_to_uris
 954      in
 955       aux 0
 956    in
 957     id_to_uris := dom,resolve_id
 958 ;;
 959
 960 let proveit () =
 961  let module L = LogicalOperations in
 962  let module G = Gdome in
 963  let notebook = (rendering_window ())#notebook in
 964  let output = (rendering_window ())#output in
 965  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
 966   match (rendering_window ())#output#get_selection with
 967     Some node ->
 968      let xpath =
 969       ((node : Gdome.element)#getAttributeNS
 970       (*CSC: OCAML DIVERGE
 971       ((element : G.element)#getAttributeNS
 972       *)
 973         ~namespaceURI:helmns
 974         ~localName:(G.domString "xref"))#to_string
 975      in
 976       if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 977       else
 978        begin
 979         try
 980          match !current_cic_infos with
 981             Some (ids_to_terms, ids_to_father_ids, _, _) ->
 982              let id = xpath in
 983               L.to_sequent id ids_to_terms ids_to_father_ids ;
 984               refresh_proof output ;
 985               refresh_sequent notebook
 986           | None -> assert false (* "ERROR: No current term!!!" *)
 987         with
 988            RefreshSequentException e ->
 989             output_html outputhtml
 990              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 991               "sequent: " ^ Printexc.to_string e ^ "</h1>")
 992          | RefreshProofException e ->
 993             output_html outputhtml
 994              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 995               "proof: " ^ Printexc.to_string e ^ "</h1>")
 996          | e ->
 997             output_html outputhtml
 998              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 999        end
1000   | None -> assert false (* "ERROR: No selection!!!" *)
1001 ;;
1002
1003 let focus () =
1004  let module L = LogicalOperations in
1005  let module G = Gdome in
1006  let notebook = (rendering_window ())#notebook in
1007  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1008   match (rendering_window ())#output#get_selection with
1009     Some node ->
1010      let xpath =
1011       ((node : Gdome.element)#getAttributeNS
1012       (*CSC: OCAML DIVERGE
1013       ((element : G.element)#getAttributeNS
1014       *)
1015         ~namespaceURI:helmns
1016         ~localName:(G.domString "xref"))#to_string
1017      in
1018       if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1019       else
1020        begin
1021         try
1022          match !current_cic_infos with
1023             Some (ids_to_terms, ids_to_father_ids, _, _) ->
1024              let id = xpath in
1025               L.focus id ids_to_terms ids_to_father_ids ;
1026               refresh_sequent notebook
1027           | None -> assert false (* "ERROR: No current term!!!" *)
1028         with
1029            RefreshSequentException e ->
1030             output_html outputhtml
1031              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1032               "sequent: " ^ Printexc.to_string e ^ "</h1>")
1033          | RefreshProofException e ->
1034             output_html outputhtml
1035              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1036               "proof: " ^ Printexc.to_string e ^ "</h1>")
1037          | e ->
1038             output_html outputhtml
1039              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1040        end
1041   | None -> assert false (* "ERROR: No selection!!!" *)
1042 ;;
1043
1044 exception NoPrevGoal;;
1045 exception NoNextGoal;;
1046
1047 let setgoal metano =
1048  let module L = LogicalOperations in
1049  let module G = Gdome in
1050  let notebook = (rendering_window ())#notebook in
1051  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1052   let metasenv =
1053    match !ProofEngine.proof with
1054       None -> assert false
1055     | Some (_,metasenv,_,_) -> metasenv
1056   in
1057    try
1058     refresh_sequent ~empty_notebook:false notebook
1059    with
1060       RefreshSequentException e ->
1061        output_html outputhtml
1062         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1063          "sequent: " ^ Printexc.to_string e ^ "</h1>")
1064     | e ->
1065        output_html outputhtml
1066         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1067 ;;
1068
1069 let show_in_show_window, show_in_show_window_callback =
1070  let window =
1071   GWindow.window ~width:800 ~border_width:2 () in
1072  let scrolled_window =
1073   GBin.scrolled_window ~border_width:10 ~packing:window#add () in
1074  let mmlwidget =
1075   GMathView.math_view ~packing:scrolled_window#add ~width:600 ~height:400 () in
1076  let _ = window#event#connect#delete (fun _ -> window#misc#hide () ; true ) in
1077  let href = Gdome.domString "href" in
1078   let show_in_show_window uri =
1079    let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1080     try
1081      CicTypeChecker.typecheck uri ;
1082      let obj = CicEnvironment.get_cooked_obj uri in
1083       let
1084        (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
1085         ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
1086       =
1087        Cic2acic.acic_object_of_cic_object obj
1088       in
1089        let mml =
1090         mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts
1091          ids_to_inner_types
1092        in
1093         window#set_title (UriManager.string_of_uri uri) ;
1094         window#misc#hide () ; window#show () ;
1095         mmlwidget#load_tree mml ;
1096     with
1097      e ->
1098       output_html outputhtml
1099        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1100   in
1101    let show_in_show_window_callback mmlwidget (n : Gdome.element) =
1102     if n#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then
1103      let uri =
1104       (n#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string
1105      in
1106       show_in_show_window (UriManager.uri_of_string uri)
1107     else
1108      if mmlwidget#get_action <> None then
1109       mmlwidget#action_toggle
1110    in
1111     let _ =
1112      mmlwidget#connect#clicked (show_in_show_window_callback mmlwidget)
1113     in
1114      show_in_show_window, show_in_show_window_callback
1115 ;;
1116
1117 exception NoObjectsLocated;;
1118
1119 let user_uri_choice ~title ~msg uris =
1120  let uri =
1121   match uris with
1122      [] -> raise NoObjectsLocated
1123    | [uri] -> uri
1124    | uris ->
1125       match
1126        interactive_user_uri_choice ~selection_mode:`SINGLE ~title ~msg uris
1127       with
1128          [uri] -> uri
1129        | _ -> assert false
1130  in
1131   String.sub uri 4 (String.length uri - 4)
1132 ;;
1133
1134 let locate_callback id =
1135  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1136  let result = MQueryGenerator.locate id in
1137  let uris =
1138   List.map
1139    (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
1140    result in
1141  let html =
1142   (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>")
1143  in
1144   output_html outputhtml html ;
1145   user_uri_choice ~title:"Ambiguous input."
1146    ~msg:
1147      ("Ambiguous input \"" ^ id ^
1148       "\". Please, choose one interpetation:")
1149    uris
1150 ;;
1151
1152 let locate () =
1153  let inputt = ((rendering_window ())#inputt : term_editor) in
1154  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1155    try
1156     match
1157      GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:"
1158     with
1159        None -> raise NoChoice
1160      | Some input ->
1161         let uri = locate_callback input in
1162          inputt#set_term uri
1163    with
1164     e ->
1165      output_html outputhtml
1166       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1167 ;;
1168
1169 let input_or_locate_uri ~title =
1170  let uri = ref None in
1171  let window =
1172   GWindow.window
1173    ~width:400 ~modal:true ~title ~border_width:2 () in
1174  let vbox = GPack.vbox ~packing:window#add () in
1175  let hbox1 =
1176   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1177  let _ =
1178   GMisc.label ~text:"Enter a valid URI:" ~packing:(hbox1#pack ~padding:5) () in
1179  let manual_input =
1180   GEdit.entry ~editable:true
1181    ~packing:(hbox1#pack ~expand:true ~fill:true ~padding:5) () in
1182  let checkb =
1183   GButton.button ~label:"Check"
1184    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1185  let _ = checkb#misc#set_sensitive false in
1186  let hbox2 =
1187   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1188  let _ =
1189   GMisc.label ~text:"You can also enter an indentifier to locate:"
1190    ~packing:(hbox2#pack ~padding:5) () in
1191  let locate_input =
1192   GEdit.entry ~editable:true
1193    ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
1194  let locateb =
1195   GButton.button ~label:"Locate"
1196    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1197  let _ = locateb#misc#set_sensitive false in
1198  let hbox3 =
1199   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1200  let okb =
1201   GButton.button ~label:"Ok"
1202    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1203  let _ = okb#misc#set_sensitive false in
1204  let cancelb =
1205   GButton.button ~label:"Cancel"
1206    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) ()
1207  in
1208   ignore (window#connect#destroy GMain.Main.quit) ;
1209   ignore
1210    (cancelb#connect#clicked (function () -> uri := None ; window#destroy ())) ;
1211   let check_callback () =
1212    let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1213    let uri = "cic:" ^ manual_input#text in
1214     try
1215       ignore (Getter.resolve (UriManager.uri_of_string uri)) ;
1216       output_html outputhtml "<h1 color=\"Green\">OK</h1>" ;
1217       true
1218     with
1219        Getter.Unresolved ->
1220         output_html outputhtml
1221          ("<h1 color=\"Red\">URI " ^ uri ^
1222           " does not correspond to any object.</h1>") ;
1223         false
1224      | UriManager.IllFormedUri _ ->
1225         output_html outputhtml
1226          ("<h1 color=\"Red\">URI " ^ uri ^ " is not well-formed.</h1>") ;
1227         false
1228      | e ->
1229         output_html outputhtml
1230          ("<h1 color=\"Red\">" ^ Printexc.to_string e ^ "</h1>") ;
1231         false
1232   in
1233   ignore
1234    (okb#connect#clicked
1235      (function () ->
1236        if check_callback () then
1237         begin
1238          uri := Some manual_input#text ;
1239          window#destroy ()
1240         end
1241    )) ;
1242   ignore (checkb#connect#clicked (function () -> ignore (check_callback ()))) ;
1243   ignore
1244    (manual_input#connect#changed
1245      (fun _ ->
1246        if manual_input#text = "" then
1247         begin
1248          checkb#misc#set_sensitive false ;
1249          okb#misc#set_sensitive false
1250         end
1251        else
1252         begin
1253          checkb#misc#set_sensitive true ;
1254          okb#misc#set_sensitive true
1255         end));
1256   ignore
1257    (locate_input#connect#changed
1258      (fun _ -> locateb#misc#set_sensitive (locate_input#text <> ""))) ;
1259   ignore
1260    (locateb#connect#clicked
1261      (function () ->
1262        let id = locate_input#text in
1263         manual_input#set_text (locate_callback id) ;
1264         locate_input#delete_text 0 (String.length id)
1265    )) ;
1266   window#show () ;
1267   GMain.Main.main () ;
1268   match !uri with
1269      None -> raise NoChoice
1270    | Some uri -> UriManager.uri_of_string ("cic:" ^ uri)
1271 ;;
1272
1273 let locate_one_id id =
1274  let result = MQueryGenerator.locate id in
1275  let uris =
1276   List.map
1277    (function uri,_ ->
1278      wrong_xpointer_format_from_wrong_xpointer_format' uri
1279    ) result in
1280  let html= " <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>" in
1281   output_html (rendering_window ())#outputhtml html ;
1282   let uris' =
1283    match uris with
1284       [] ->
1285        [UriManager.string_of_uri
1286          (input_or_locate_uri ~title:("URI matching \"" ^ id ^ "\" unknown."))]
1287     | [uri] -> [uri]
1288     | _ ->
1289       interactive_user_uri_choice
1290        ~selection_mode:`EXTENDED
1291        ~ok:"Try every selection."
1292        ~title:"Ambiguous input."
1293        ~msg:
1294          ("Ambiguous input \"" ^ id ^
1295           "\". Please, choose one or more interpretations:")
1296        uris
1297   in
1298    List.map cic_textual_parser_uri_of_string uris'
1299 ;;
1300
1301 exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput;;
1302 exception AmbiguousInput;;
1303
1304 let disambiguate_input context metasenv dom mk_metasenv_and_expr =
1305  let known_ids,resolve_id = !id_to_uris in
1306  let dom' =
1307   let rec filter =
1308    function
1309       [] -> []
1310     | he::tl ->
1311        if List.mem he known_ids then filter tl else he::(filter tl)
1312   in
1313    filter dom
1314  in
1315   (* for each id in dom' we get the list of uris associated to it *)
1316   let list_of_uris = List.map locate_one_id dom' in
1317   (* and now we compute the list of all possible assignments from id to uris *)
1318   let resolve_ids =
1319    let rec aux ids list_of_uris =
1320     match ids,list_of_uris with
1321        [],[] -> [resolve_id]
1322      | id::idtl,uris::uristl ->
1323         let resolves = aux idtl uristl in
1324          List.concat
1325           (List.map
1326             (function uri ->
1327               List.map
1328                (function f ->
1329                  function id' -> if id = id' then Some uri else f id'
1330                ) resolves
1331             ) uris
1332           )
1333      | _,_ -> assert false
1334    in
1335     aux dom' list_of_uris
1336   in
1337    let tests_no = List.length resolve_ids in
1338     if tests_no > 1 then
1339      output_html (outputhtml ())
1340       ("<h1>Disambiguation phase started: " ^
1341         string_of_int (List.length resolve_ids) ^ " cases will be tried.") ;
1342    (* now we select only the ones that generates well-typed terms *)
1343    let resolve_ids' =
1344     let rec filter =
1345      function
1346         [] -> []
1347       | resolve::tl ->
1348          let metasenv',expr = mk_metasenv_and_expr resolve in
1349           try
1350 (*CSC: Bug here: we do not try to typecheck also the metasenv' *)
1351            ignore
1352             (CicTypeChecker.type_of_aux' metasenv context expr) ;
1353            resolve::(filter tl)
1354           with
1355            _ -> filter tl
1356     in
1357      filter resolve_ids
1358    in
1359     let resolve_id' =
1360      match resolve_ids' with
1361         [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
1362       | [resolve_id] -> resolve_id
1363       | _ ->
1364         let choices =
1365          List.map
1366           (function resolve ->
1367             List.map
1368              (function id ->
1369                id,
1370                 match resolve id with
1371                    None -> assert false
1372                  | Some uri ->
1373                     match uri with
1374                        CicTextualParser0.ConUri uri
1375                      | CicTextualParser0.VarUri uri ->
1376                         UriManager.string_of_uri uri
1377                      | CicTextualParser0.IndTyUri (uri,tyno) ->
1378                         UriManager.string_of_uri uri ^ "#xpointer(1/" ^
1379                          string_of_int (tyno+1) ^ ")"
1380                      | CicTextualParser0.IndConUri (uri,tyno,consno) ->
1381                         UriManager.string_of_uri uri ^ "#xpointer(1/" ^
1382                          string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^                           ")"
1383              ) dom
1384           ) resolve_ids'
1385         in
1386          let index = interactive_interpretation_choice choices in
1387           List.nth resolve_ids' index
1388     in
1389      id_to_uris := known_ids @ dom', resolve_id' ;
1390      mk_metasenv_and_expr resolve_id'
1391 ;;
1392
1393 exception UriAlreadyInUse;;
1394 exception NotAUriToAConstant;;
1395
1396 let new_proof () =
1397  let inputt = ((rendering_window ())#inputt : term_editor) in
1398  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1399  let output = ((rendering_window ())#output : GMathView.math_view) in
1400  let notebook = (rendering_window ())#notebook in
1401
1402  let chosen = ref false in
1403  let get_parsed = ref (function _ -> assert false) in
1404  let get_uri = ref (function _ -> assert false) in
1405  let non_empty_type = ref false in
1406  let window =
1407   GWindow.window
1408    ~width:600 ~modal:true ~title:"New Proof or Definition"
1409    ~border_width:2 () in
1410  let vbox = GPack.vbox ~packing:window#add () in
1411  let hbox =
1412   GPack.hbox ~border_width:0
1413    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1414  let _ =
1415   GMisc.label ~text:"Enter the URI for the new theorem or definition:"
1416    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1417  let uri_entry =
1418   GEdit.entry ~editable:true
1419    ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1420  let hbox1 =
1421   GPack.hbox ~border_width:0
1422    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1423  let _ =
1424   GMisc.label ~text:"Enter the theorem or definition type:"
1425    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1426  let scrolled_window =
1427   GBin.scrolled_window ~border_width:5
1428    ~packing:(vbox#pack ~expand:true ~padding:0) () in
1429  (* the content of the scrolled_window is moved below (see comment) *)
1430  let hbox =
1431   GPack.hbox ~border_width:0
1432    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1433  let okb =
1434   GButton.button ~label:"Ok"
1435    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1436  let _ = okb#misc#set_sensitive false in
1437  let cancelb =
1438   GButton.button ~label:"Cancel"
1439    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1440  (* moved here to have visibility of the ok button *)
1441  let newinputt =
1442   new term_editor ~width:400 ~height:100 ~packing:scrolled_window#add ()
1443    ~isnotempty_callback:
1444     (function b ->
1445       non_empty_type := b ;
1446       okb#misc#set_sensitive (b && uri_entry#text <> ""))
1447  in
1448  let _ =
1449   newinputt#set_term inputt#get_as_string ;
1450   inputt#reset in
1451  let _ =
1452   uri_entry#connect#changed
1453    (function () ->
1454      okb#misc#set_sensitive (!non_empty_type && uri_entry#text <> ""))
1455  in
1456  ignore (window#connect#destroy GMain.Main.quit) ;
1457  ignore (cancelb#connect#clicked window#destroy) ;
1458  ignore
1459   (okb#connect#clicked
1460     (function () ->
1461       chosen := true ;
1462       try
1463        let parsed = newinputt#get_term [] [] in
1464        let uristr = "cic:" ^ uri_entry#text in
1465        let uri = UriManager.uri_of_string uristr in
1466         if String.sub uristr (String.length uristr - 4) 4 <> ".con" then
1467          raise NotAUriToAConstant
1468         else
1469          begin
1470           try
1471            ignore (Getter.resolve uri) ;
1472            raise UriAlreadyInUse
1473           with
1474            Getter.Unresolved ->
1475             get_parsed := (function () -> parsed) ;
1476             get_uri := (function () -> uri) ;
1477             window#destroy ()
1478          end
1479       with
1480        e ->
1481         output_html outputhtml
1482          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1483   )) ;
1484  window#show () ;
1485  GMain.Main.main () ;
1486  if !chosen then
1487   try
1488    let dom,mk_metasenv_and_expr = !get_parsed () in
1489     let metasenv,expr =
1490      disambiguate_input [] [] dom mk_metasenv_and_expr
1491     in
1492      let _  = CicTypeChecker.type_of_aux' metasenv [] expr in
1493       ProofEngine.proof :=
1494        Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
1495       ProofEngine.goal := Some 1 ;
1496       refresh_sequent notebook ;
1497       refresh_proof output ;
1498       !save_set_sensitive true ;
1499       inputt#reset
1500   with
1501      RefreshSequentException e ->
1502       output_html outputhtml
1503        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1504         "sequent: " ^ Printexc.to_string e ^ "</h1>")
1505    | RefreshProofException e ->
1506       output_html outputhtml
1507        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1508         "proof: " ^ Printexc.to_string e ^ "</h1>")
1509    | e ->
1510       output_html outputhtml
1511        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1512 ;;
1513
1514 let check_term_in_scratch scratch_window metasenv context expr =
1515  try
1516   let ty  = CicTypeChecker.type_of_aux' metasenv context expr in
1517    let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
1518 prerr_endline ("### " ^ CicPp.ppterm expr ^ " ==> " ^ CicPp.ppterm ty) ;
1519     scratch_window#show () ;
1520     scratch_window#mmlwidget#load_tree ~dom:mml
1521  with
1522   e ->
1523    print_endline ("? " ^ CicPp.ppterm expr) ;
1524    raise e
1525 ;;
1526
1527 let check scratch_window () =
1528  let inputt = ((rendering_window ())#inputt : term_editor) in
1529  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1530   let metasenv =
1531    match !ProofEngine.proof with
1532       None -> []
1533     | Some (_,metasenv,_,_) -> metasenv
1534   in
1535   let context,names_context =
1536    let context =
1537     match !ProofEngine.goal with
1538        None -> []
1539      | Some metano ->
1540         let (_,canonical_context,_) =
1541          List.find (function (m,_,_) -> m=metano) metasenv
1542         in
1543          canonical_context
1544    in
1545     context,
1546     List.map
1547      (function
1548          Some (n,_) -> Some n
1549        | None -> None
1550      ) context
1551   in
1552    try
1553     let dom,mk_metasenv_and_expr = inputt#get_term names_context metasenv in
1554      let (metasenv',expr) =
1555       disambiguate_input context metasenv dom mk_metasenv_and_expr
1556      in
1557       check_term_in_scratch scratch_window metasenv' context expr
1558    with
1559     e ->
1560      output_html outputhtml
1561       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1562 ;;
1563
1564
1565 (***********************)
1566 (*       TACTICS       *)
1567 (***********************)
1568
1569 let call_tactic tactic () =
1570  let notebook = (rendering_window ())#notebook in
1571  let output = ((rendering_window ())#output : GMathView.math_view) in
1572  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1573  let savedproof = !ProofEngine.proof in
1574  let savedgoal  = !ProofEngine.goal in
1575   begin
1576    try
1577     tactic () ;
1578     refresh_sequent notebook ;
1579     refresh_proof output
1580    with
1581       RefreshSequentException e ->
1582        output_html outputhtml
1583         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1584          "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1585        ProofEngine.proof := savedproof ;
1586        ProofEngine.goal := savedgoal ;
1587        refresh_sequent notebook
1588     | RefreshProofException e ->
1589        output_html outputhtml
1590         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1591          "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1592        ProofEngine.proof := savedproof ;
1593        ProofEngine.goal := savedgoal ;
1594        refresh_sequent notebook ;
1595        refresh_proof output
1596     | e ->
1597        output_html outputhtml
1598         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1599        ProofEngine.proof := savedproof ;
1600        ProofEngine.goal := savedgoal ;
1601   end
1602 ;;
1603
1604 let call_tactic_with_input tactic () =
1605  let notebook = (rendering_window ())#notebook in
1606  let output = ((rendering_window ())#output : GMathView.math_view) in
1607  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1608  let inputt = ((rendering_window ())#inputt : term_editor) in
1609  let savedproof = !ProofEngine.proof in
1610  let savedgoal  = !ProofEngine.goal in
1611   let uri,metasenv,bo,ty =
1612    match !ProofEngine.proof with
1613       None -> assert false
1614     | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
1615   in
1616    let canonical_context =
1617     match !ProofEngine.goal with
1618        None -> assert false
1619      | Some metano ->
1620         let (_,canonical_context,_) =
1621          List.find (function (m,_,_) -> m=metano) metasenv
1622         in
1623          canonical_context
1624    in
1625    let context =
1626     List.map
1627      (function
1628          Some (n,_) -> Some n
1629        | None -> None
1630      ) canonical_context
1631    in
1632     try
1633      let dom,mk_metasenv_and_expr = inputt#get_term context metasenv in
1634       let (metasenv',expr) =
1635        disambiguate_input canonical_context metasenv dom mk_metasenv_and_expr
1636       in
1637        ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
1638        tactic expr ;
1639        refresh_sequent notebook ;
1640        refresh_proof output ;
1641        inputt#reset
1642     with
1643        RefreshSequentException e ->
1644         output_html outputhtml
1645          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1646           "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1647         ProofEngine.proof := savedproof ;
1648         ProofEngine.goal := savedgoal ;
1649         refresh_sequent notebook
1650      | RefreshProofException e ->
1651         output_html outputhtml
1652          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1653           "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1654         ProofEngine.proof := savedproof ;
1655         ProofEngine.goal := savedgoal ;
1656         refresh_sequent notebook ;
1657         refresh_proof output
1658      | e ->
1659         output_html outputhtml
1660          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1661         ProofEngine.proof := savedproof ;
1662         ProofEngine.goal := savedgoal ;
1663 ;;
1664
1665 let call_tactic_with_goal_input tactic () =
1666  let module L = LogicalOperations in
1667  let module G = Gdome in
1668   let notebook = (rendering_window ())#notebook in
1669   let output = ((rendering_window ())#output : GMathView.math_view) in
1670   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1671   let savedproof = !ProofEngine.proof in
1672   let savedgoal  = !ProofEngine.goal in
1673    match notebook#proofw#get_selection with
1674      Some node ->
1675       let xpath =
1676        ((node : Gdome.element)#getAttributeNS
1677          ~namespaceURI:helmns
1678          ~localName:(G.domString "xref"))#to_string
1679       in
1680        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1681        else
1682         begin
1683          try
1684           match !current_goal_infos with
1685              Some (ids_to_terms, ids_to_father_ids,_) ->
1686               let id = xpath in
1687                tactic (Hashtbl.find ids_to_terms id) ;
1688                refresh_sequent notebook ;
1689                refresh_proof output
1690            | None -> assert false (* "ERROR: No current term!!!" *)
1691          with
1692             RefreshSequentException e ->
1693              output_html outputhtml
1694               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1695                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1696              ProofEngine.proof := savedproof ;
1697              ProofEngine.goal := savedgoal ;
1698              refresh_sequent notebook
1699           | RefreshProofException e ->
1700              output_html outputhtml
1701               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1702                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1703              ProofEngine.proof := savedproof ;
1704              ProofEngine.goal := savedgoal ;
1705              refresh_sequent notebook ;
1706              refresh_proof output
1707           | e ->
1708              output_html outputhtml
1709               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1710              ProofEngine.proof := savedproof ;
1711              ProofEngine.goal := savedgoal ;
1712         end
1713    | None ->
1714       output_html outputhtml
1715        ("<h1 color=\"red\">No term selected</h1>")
1716 ;;
1717
1718 let call_tactic_with_input_and_goal_input tactic () =
1719  let module L = LogicalOperations in
1720  let module G = Gdome in
1721   let notebook = (rendering_window ())#notebook in
1722   let output = ((rendering_window ())#output : GMathView.math_view) in
1723   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1724   let inputt = ((rendering_window ())#inputt : term_editor) in
1725   let savedproof = !ProofEngine.proof in
1726   let savedgoal  = !ProofEngine.goal in
1727    match notebook#proofw#get_selection with
1728      Some node ->
1729       let xpath =
1730        ((node : Gdome.element)#getAttributeNS
1731          ~namespaceURI:helmns
1732          ~localName:(G.domString "xref"))#to_string
1733       in
1734        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1735        else
1736         begin
1737          try
1738           match !current_goal_infos with
1739              Some (ids_to_terms, ids_to_father_ids,_) ->
1740               let id = xpath in
1741                let uri,metasenv,bo,ty =
1742                 match !ProofEngine.proof with
1743                    None -> assert false
1744                  | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
1745                in
1746                 let canonical_context =
1747                  match !ProofEngine.goal with
1748                     None -> assert false
1749                   | Some metano ->
1750                      let (_,canonical_context,_) =
1751                       List.find (function (m,_,_) -> m=metano) metasenv
1752                      in
1753                       canonical_context in
1754                 let context =
1755                  List.map
1756                   (function
1757                       Some (n,_) -> Some n
1758                     | None -> None
1759                   ) canonical_context
1760                 in
1761                  let dom,mk_metasenv_and_expr = inputt#get_term context metasenv
1762                  in
1763                   let (metasenv',expr) =
1764                    disambiguate_input canonical_context metasenv dom
1765                     mk_metasenv_and_expr
1766                   in
1767                    ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
1768                    tactic ~goal_input:(Hashtbl.find ids_to_terms id)
1769                     ~input:expr ;
1770                    refresh_sequent notebook ;
1771                    refresh_proof output ;
1772                    inputt#reset
1773            | None -> assert false (* "ERROR: No current term!!!" *)
1774          with
1775             RefreshSequentException e ->
1776              output_html outputhtml
1777               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1778                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1779              ProofEngine.proof := savedproof ;
1780              ProofEngine.goal := savedgoal ;
1781              refresh_sequent notebook
1782           | RefreshProofException e ->
1783              output_html outputhtml
1784               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1785                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1786              ProofEngine.proof := savedproof ;
1787              ProofEngine.goal := savedgoal ;
1788              refresh_sequent notebook ;
1789              refresh_proof output
1790           | e ->
1791              output_html outputhtml
1792               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1793              ProofEngine.proof := savedproof ;
1794              ProofEngine.goal := savedgoal ;
1795         end
1796    | None ->
1797       output_html outputhtml
1798        ("<h1 color=\"red\">No term selected</h1>")
1799 ;;
1800
1801 let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
1802  let module L = LogicalOperations in
1803  let module G = Gdome in
1804   let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in
1805   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1806   let savedproof = !ProofEngine.proof in
1807   let savedgoal  = !ProofEngine.goal in
1808    match mmlwidget#get_selection with
1809      Some node ->
1810       let xpath =
1811        ((node : Gdome.element)#getAttributeNS
1812          ~namespaceURI:helmns
1813          ~localName:(G.domString "xref"))#to_string
1814       in
1815        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1816        else
1817         begin
1818          try
1819           match !current_scratch_infos with
1820              (* term is the whole goal in the scratch_area *)
1821              Some (term,ids_to_terms, ids_to_father_ids,_) ->
1822               let id = xpath in
1823                let expr = tactic term (Hashtbl.find ids_to_terms id) in
1824                 let mml = mml_of_cic_term 111 expr in
1825                  scratch_window#show () ;
1826                  scratch_window#mmlwidget#load_tree ~dom:mml
1827            | None -> assert false (* "ERROR: No current term!!!" *)
1828          with
1829           e ->
1830            output_html outputhtml
1831             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1832         end
1833    | None ->
1834       output_html outputhtml
1835        ("<h1 color=\"red\">No term selected</h1>")
1836 ;;
1837
1838 let call_tactic_with_hypothesis_input tactic () =
1839  let module L = LogicalOperations in
1840  let module G = Gdome in
1841   let notebook = (rendering_window ())#notebook in
1842   let output = ((rendering_window ())#output : GMathView.math_view) in
1843   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1844   let savedproof = !ProofEngine.proof in
1845   let savedgoal  = !ProofEngine.goal in
1846    match notebook#proofw#get_selection with
1847      Some node ->
1848       let xpath =
1849        ((node : Gdome.element)#getAttributeNS
1850          ~namespaceURI:helmns
1851          ~localName:(G.domString "xref"))#to_string
1852       in
1853        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1854        else
1855         begin
1856          try
1857           match !current_goal_infos with
1858              Some (_,_,ids_to_hypotheses) ->
1859               let id = xpath in
1860                tactic (Hashtbl.find ids_to_hypotheses id) ;
1861                refresh_sequent notebook ;
1862                refresh_proof output
1863            | None -> assert false (* "ERROR: No current term!!!" *)
1864          with
1865             RefreshSequentException e ->
1866              output_html outputhtml
1867               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1868                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1869              ProofEngine.proof := savedproof ;
1870              ProofEngine.goal := savedgoal ;
1871              refresh_sequent notebook
1872           | RefreshProofException e ->
1873              output_html outputhtml
1874               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1875                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1876              ProofEngine.proof := savedproof ;
1877              ProofEngine.goal := savedgoal ;
1878              refresh_sequent notebook ;
1879              refresh_proof output
1880           | e ->
1881              output_html outputhtml
1882               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1883              ProofEngine.proof := savedproof ;
1884              ProofEngine.goal := savedgoal ;
1885         end
1886    | None ->
1887       output_html outputhtml
1888        ("<h1 color=\"red\">No term selected</h1>")
1889 ;;
1890
1891
1892 let intros = call_tactic ProofEngine.intros;;
1893 let exact = call_tactic_with_input ProofEngine.exact;;
1894 let apply = call_tactic_with_input ProofEngine.apply;;
1895 let elimsimplintros = call_tactic_with_input ProofEngine.elim_simpl_intros;;
1896 let elimtype = call_tactic_with_input ProofEngine.elim_type;;
1897 let whd = call_tactic_with_goal_input ProofEngine.whd;;
1898 let reduce = call_tactic_with_goal_input ProofEngine.reduce;;
1899 let simpl = call_tactic_with_goal_input ProofEngine.simpl;;
1900 let fold = call_tactic_with_input ProofEngine.fold;;
1901 let cut = call_tactic_with_input ProofEngine.cut;;
1902 let change = call_tactic_with_input_and_goal_input ProofEngine.change;;
1903 let letin = call_tactic_with_input ProofEngine.letin;;
1904 let ring = call_tactic ProofEngine.ring;;
1905 let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody;;
1906 let clear = call_tactic_with_hypothesis_input ProofEngine.clear;;
1907 let fourier = call_tactic ProofEngine.fourier;;
1908 let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl;;
1909 let reflexivity = call_tactic ProofEngine.reflexivity;;
1910 let symmetry = call_tactic ProofEngine.symmetry;;
1911 let transitivity = call_tactic_with_input ProofEngine.transitivity;;
1912 let left = call_tactic ProofEngine.left;;
1913 let right = call_tactic ProofEngine.right;;
1914 let assumption = call_tactic ProofEngine.assumption;;
1915
1916 let whd_in_scratch scratch_window =
1917  call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
1918   scratch_window
1919 ;;
1920 let reduce_in_scratch scratch_window =
1921  call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch
1922   scratch_window
1923 ;;
1924 let simpl_in_scratch scratch_window =
1925  call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch
1926   scratch_window
1927 ;;
1928
1929
1930
1931 (**********************)
1932 (*   END OF TACTICS   *)
1933 (**********************)
1934
1935
1936 let show () =
1937  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1938   try
1939    show_in_show_window (input_or_locate_uri ~title:"Show")
1940   with
1941    e ->
1942     output_html outputhtml
1943      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1944 ;;
1945
1946 exception NotADefinition;;
1947
1948 let open_ () =
1949  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1950  let output = ((rendering_window ())#output : GMathView.math_view) in
1951  let notebook = (rendering_window ())#notebook in
1952    try
1953     let uri = input_or_locate_uri ~title:"Open" in
1954      CicTypeChecker.typecheck uri ;
1955      let metasenv,bo,ty =
1956       match CicEnvironment.get_cooked_obj uri with
1957          Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
1958        | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
1959        | Cic.Constant _
1960        | Cic.Variable _
1961        | Cic.InductiveDefinition _ -> raise NotADefinition
1962      in
1963       ProofEngine.proof :=
1964        Some (uri, metasenv, bo, ty) ;
1965       ProofEngine.goal := None ;
1966       refresh_sequent notebook ;
1967       refresh_proof output
1968    with
1969       RefreshSequentException e ->
1970        output_html outputhtml
1971         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1972          "sequent: " ^ Printexc.to_string e ^ "</h1>")
1973     | RefreshProofException e ->
1974        output_html outputhtml
1975         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1976          "proof: " ^ Printexc.to_string e ^ "</h1>")
1977     | e ->
1978        output_html outputhtml
1979         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1980 ;;
1981
1982
1983 let searchPattern () =
1984  let inputt = ((rendering_window ())#inputt : term_editor) in
1985  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1986   try
1987    let rec get_level ?(last_invalid=false) () =
1988     match
1989      GToolbox.input_string
1990       ~title:"Insert the strictness parameter for the query:"
1991       ((if last_invalid then
1992          "Invalid input (must be a non-negative natural number). Insert again "
1993         else
1994          "Insert "
1995        ) ^ "the strictness parameter for the query:")
1996     with
1997        None -> raise NoChoice
1998      | Some n ->
1999         try
2000          int_of_string n
2001         with
2002          _ -> get_level ~last_invalid:true ()
2003    in
2004     let level = get_level () in
2005     let metasenv =
2006      match !ProofEngine.proof with
2007         None -> assert false
2008       | Some (_,metasenv,_,_) -> metasenv
2009     in
2010      match !ProofEngine.goal with
2011         None -> ()
2012       | Some metano ->
2013          let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
2014           let list_of_must,can = MQueryLevels.out_restr metasenv ey ty in
2015           let len = List.length list_of_must in
2016           let must = if level < len then List.nth list_of_must level else can in
2017           let result = MQueryGenerator.searchPattern metasenv ey ty must can in
2018           let uris =
2019            List.map
2020             (function uri,_ ->
2021               wrong_xpointer_format_from_wrong_xpointer_format' uri
2022             ) result in
2023           let html =
2024            " <h1>Backward Query: </h1>" ^
2025            " <h2>Levels: </h2> " ^
2026            MQueryLevels.string_of_levels
2027             (MQueryLevels.levels_of_term metasenv ey ty) "<br>" ^
2028            " <pre>" ^ get_last_query result ^ "</pre>"
2029           in
2030            output_html outputhtml html ;
2031            let uris',exc =
2032             let rec filter_out =
2033              function
2034                 [] -> [],""
2035               | uri::tl ->
2036                  let tl',exc = filter_out tl in
2037                   try
2038                    if
2039                     ProofEngine.can_apply
2040                      (term_of_cic_textual_parser_uri
2041                       (cic_textual_parser_uri_of_string uri))
2042                    then
2043                     uri::tl',exc
2044                    else
2045                     tl',exc
2046                   with
2047                    e ->
2048                     let exc' =
2049                      "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
2050                       uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
2051                     in
2052                      tl',exc'
2053             in
2054              filter_out uris
2055            in
2056             let html' =
2057              " <h1>Objects that can actually be applied: </h1> " ^
2058              String.concat "<br>" uris' ^ exc ^
2059              " <h1>Number of false matches: " ^
2060               string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
2061              " <h1>Number of good matches: " ^
2062               string_of_int (List.length uris') ^ "</h1>"
2063             in
2064              output_html outputhtml html' ;
2065              let uri' =
2066               user_uri_choice ~title:"Ambiguous input."
2067               ~msg:
2068                 "Many lemmas can be successfully applied. Please, choose one:"
2069                uris'
2070              in
2071               inputt#set_term uri' ;
2072               apply ()
2073   with
2074    e ->
2075     output_html outputhtml
2076      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2077 ;;
2078
2079 let choose_selection
2080      (mmlwidget : GMathView.math_view) (element : Gdome.element option)
2081 =
2082  let module G = Gdome in
2083   let rec aux element =
2084    if element#hasAttributeNS
2085        ~namespaceURI:helmns
2086        ~localName:(G.domString "xref")
2087    then
2088      mmlwidget#set_selection (Some element)
2089    else
2090       match element#get_parentNode with
2091          None -> assert false
2092        (*CSC: OCAML DIVERGES!
2093        | Some p -> aux (new G.element_of_node p)
2094        *)
2095        | Some p -> aux (new Gdome.element_of_node p)
2096   in
2097    match element with
2098      Some x -> aux x
2099    | None   -> mmlwidget#set_selection None
2100 ;;
2101
2102 (* STUFF TO BUILD THE GTK INTERFACE *)
2103
2104 (* Stuff for the widget settings *)
2105
2106 let export_to_postscript (output : GMathView.math_view) =
2107  let lastdir = ref (Unix.getcwd ()) in
2108   function () ->
2109    match
2110     GToolbox.select_file ~title:"Export to PostScript"
2111      ~dir:lastdir ~filename:"screenshot.ps" ()
2112    with
2113       None -> ()
2114     | Some filename ->
2115        output#export_to_postscript ~filename:filename ();
2116 ;;
2117
2118 let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
2119  button_set_kerning button_set_transparency export_to_postscript_menu_item
2120  button_t1 ()
2121 =
2122  let is_set = button_t1#active in
2123   output#set_font_manager_type
2124    (if is_set then `font_manager_t1 else `font_manager_gtk) ;
2125   if is_set then
2126    begin
2127     button_set_anti_aliasing#misc#set_sensitive true ;
2128     button_set_kerning#misc#set_sensitive true ;
2129     button_set_transparency#misc#set_sensitive true ;
2130     export_to_postscript_menu_item#misc#set_sensitive true ;
2131    end
2132   else
2133    begin
2134     button_set_anti_aliasing#misc#set_sensitive false ;
2135     button_set_kerning#misc#set_sensitive false ;
2136     button_set_transparency#misc#set_sensitive false ;
2137     export_to_postscript_menu_item#misc#set_sensitive false ;
2138    end
2139 ;;
2140
2141 let set_anti_aliasing output button_set_anti_aliasing () =
2142  output#set_anti_aliasing button_set_anti_aliasing#active
2143 ;;
2144
2145 let set_kerning output button_set_kerning () =
2146  output#set_kerning button_set_kerning#active
2147 ;;
2148
2149 let set_transparency output button_set_transparency () =
2150  output#set_transparency button_set_transparency#active
2151 ;;
2152
2153 let changefont output font_size_spinb () =
2154  output#set_font_size font_size_spinb#value_as_int
2155 ;;
2156
2157 let set_log_verbosity output log_verbosity_spinb () =
2158  output#set_log_verbosity log_verbosity_spinb#value_as_int
2159 ;;
2160
2161 class settings_window (output : GMathView.math_view) sw
2162  export_to_postscript_menu_item selection_changed_callback
2163 =
2164  let settings_window = GWindow.window ~title:"GtkMathView settings" () in
2165  let vbox =
2166   GPack.vbox ~packing:settings_window#add () in
2167  let table =
2168   GPack.table
2169    ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
2170    ~border_width:5 ~packing:vbox#add () in
2171  let button_t1 =
2172   GButton.toggle_button ~label:"activate t1 fonts"
2173    ~packing:(table#attach ~left:0 ~top:0) () in
2174  let button_set_anti_aliasing =
2175   GButton.toggle_button ~label:"set_anti_aliasing"
2176    ~packing:(table#attach ~left:0 ~top:1) () in
2177  let button_set_kerning =
2178   GButton.toggle_button ~label:"set_kerning"
2179    ~packing:(table#attach ~left:1 ~top:1) () in
2180  let button_set_transparency =
2181   GButton.toggle_button ~label:"set_transparency"
2182    ~packing:(table#attach ~left:2 ~top:1) () in
2183  let table =
2184   GPack.table
2185    ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
2186    ~border_width:5 ~packing:vbox#add () in
2187  let font_size_label =
2188   GMisc.label ~text:"font size:"
2189    ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
2190  let font_size_spinb =
2191   let sadj =
2192    GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
2193   in
2194    GEdit.spin_button
2195     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
2196  let log_verbosity_label =
2197   GMisc.label ~text:"log verbosity:"
2198    ~packing:(table#attach ~left:0 ~top:1) () in
2199  let log_verbosity_spinb =
2200   let sadj =
2201    GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
2202   in
2203    GEdit.spin_button
2204     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
2205  let hbox =
2206   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2207  let closeb =
2208   GButton.button ~label:"Close"
2209    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2210 object(self)
2211  method show = settings_window#show
2212  initializer
2213   button_set_anti_aliasing#misc#set_sensitive false ;
2214   button_set_kerning#misc#set_sensitive false ;
2215   button_set_transparency#misc#set_sensitive false ;
2216   (* Signals connection *)
2217   ignore(button_t1#connect#clicked
2218    (activate_t1 output button_set_anti_aliasing button_set_kerning
2219     button_set_transparency export_to_postscript_menu_item button_t1)) ;
2220   ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
2221   ignore(button_set_anti_aliasing#connect#toggled
2222    (set_anti_aliasing output button_set_anti_aliasing));
2223   ignore(button_set_kerning#connect#toggled
2224    (set_kerning output button_set_kerning)) ;
2225   ignore(button_set_transparency#connect#toggled
2226    (set_transparency output button_set_transparency)) ;
2227   ignore(log_verbosity_spinb#connect#changed
2228    (set_log_verbosity output log_verbosity_spinb)) ;
2229   ignore(closeb#connect#clicked settings_window#misc#hide)
2230 end;;
2231
2232 (* Scratch window *)
2233
2234 class scratch_window =
2235  let window =
2236   GWindow.window ~title:"MathML viewer" ~border_width:2 () in
2237  let vbox =
2238   GPack.vbox ~packing:window#add () in
2239  let hbox =
2240   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2241  let whdb =
2242   GButton.button ~label:"Whd"
2243    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2244  let reduceb =
2245   GButton.button ~label:"Reduce"
2246    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2247  let simplb =
2248   GButton.button ~label:"Simpl"
2249    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2250  let scrolled_window =
2251   GBin.scrolled_window ~border_width:10
2252    ~packing:(vbox#pack ~expand:true ~padding:5) () in
2253  let mmlwidget =
2254   GMathView.math_view
2255    ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
2256 object(self)
2257  method mmlwidget = mmlwidget
2258  method show () = window#misc#hide () ; window#show ()
2259  initializer
2260   ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
2261   ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
2262   ignore(whdb#connect#clicked (whd_in_scratch self)) ;
2263   ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
2264   ignore(simplb#connect#clicked (simpl_in_scratch self))
2265 end;;
2266
2267 class page () =
2268  let vbox1 = GPack.vbox () in
2269 object(self)
2270  val mutable proofw_ref = None
2271  val mutable compute_ref = None
2272  method proofw =
2273   Lazy.force self#compute ;
2274   match proofw_ref with
2275      None -> assert false
2276    | Some proofw -> proofw
2277  method content = vbox1
2278  method compute =
2279   match compute_ref with
2280      None -> assert false
2281    | Some compute -> compute
2282  initializer
2283   compute_ref <-
2284    Some (lazy (
2285    let scrolled_window1 =
2286     GBin.scrolled_window ~border_width:10
2287      ~packing:(vbox1#pack ~expand:true ~padding:5) () in
2288    let proofw =
2289     GMathView.math_view ~width:400 ~height:275
2290      ~packing:(scrolled_window1#add) () in
2291    let _ = proofw_ref <- Some proofw in
2292    let hbox3 =
2293     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
2294    let exactb =
2295     GButton.button ~label:"Exact"
2296      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2297    let introsb =
2298     GButton.button ~label:"Intros"
2299      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2300    let applyb =
2301     GButton.button ~label:"Apply"
2302      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2303    let elimsimplintrosb =
2304     GButton.button ~label:"ElimSimplIntros"
2305      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2306    let elimtypeb =
2307     GButton.button ~label:"ElimType"
2308      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2309    let whdb =
2310     GButton.button ~label:"Whd"
2311      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2312    let reduceb =
2313     GButton.button ~label:"Reduce"
2314      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2315    let simplb =
2316     GButton.button ~label:"Simpl"
2317      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2318    let foldb =
2319     GButton.button ~label:"Fold"
2320      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2321    let cutb =
2322     GButton.button ~label:"Cut"
2323      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2324    let hbox4 =
2325     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
2326    let changeb =
2327     GButton.button ~label:"Change"
2328      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2329    let letinb =
2330     GButton.button ~label:"Let ... In"
2331      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2332    let ringb =
2333     GButton.button ~label:"Ring"
2334      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2335    let clearbodyb =
2336     GButton.button ~label:"ClearBody"
2337      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2338    let clearb =
2339     GButton.button ~label:"Clear"
2340      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2341    let fourierb =
2342     GButton.button ~label:"Fourier"
2343      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2344    let rewritesimplb =
2345     GButton.button ~label:"RewriteSimpl ->"
2346      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2347    let reflexivityb =
2348     GButton.button ~label:"Reflexivity"
2349      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2350    let hbox5 =
2351     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
2352    let symmetryb =
2353     GButton.button ~label:"Symmetry"
2354      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2355    let transitivityb =
2356     GButton.button ~label:"Transitivity"
2357      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2358    let leftb =
2359     GButton.button ~label:"Left"
2360      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2361    let rightb =
2362     GButton.button ~label:"Right"
2363      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2364    let assumptionb =
2365     GButton.button ~label:"Assumption"
2366      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2367    let searchpatternb =
2368     GButton.button ~label:"SearchPattern_Apply"
2369      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2370    ignore(exactb#connect#clicked exact) ;
2371    ignore(applyb#connect#clicked apply) ;
2372    ignore(elimsimplintrosb#connect#clicked elimsimplintros) ;
2373    ignore(elimtypeb#connect#clicked elimtype) ;
2374    ignore(whdb#connect#clicked whd) ;
2375    ignore(reduceb#connect#clicked reduce) ;
2376    ignore(simplb#connect#clicked simpl) ;
2377    ignore(foldb#connect#clicked fold) ;
2378    ignore(cutb#connect#clicked cut) ;
2379    ignore(changeb#connect#clicked change) ;
2380    ignore(letinb#connect#clicked letin) ;
2381    ignore(ringb#connect#clicked ring) ;
2382    ignore(clearbodyb#connect#clicked clearbody) ;
2383    ignore(clearb#connect#clicked clear) ;
2384    ignore(fourierb#connect#clicked fourier) ;
2385    ignore(rewritesimplb#connect#clicked rewritesimpl) ;
2386    ignore(reflexivityb#connect#clicked reflexivity) ;
2387    ignore(symmetryb#connect#clicked symmetry) ;
2388    ignore(transitivityb#connect#clicked transitivity) ;
2389    ignore(leftb#connect#clicked left) ;
2390    ignore(rightb#connect#clicked right) ;
2391    ignore(assumptionb#connect#clicked assumption) ;
2392    ignore(introsb#connect#clicked intros) ;
2393    ignore(searchpatternb#connect#clicked searchPattern) ;
2394    ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
2395   ))
2396 end
2397 ;;
2398
2399 class empty_page =
2400  let vbox1 = GPack.vbox () in
2401  let scrolled_window1 =
2402   GBin.scrolled_window ~border_width:10
2403    ~packing:(vbox1#pack ~expand:true ~padding:5) () in
2404  let proofw =
2405   GMathView.math_view ~width:400 ~height:275
2406    ~packing:(scrolled_window1#add) () in
2407 object(self)
2408  method proofw = (assert false : GMathView.math_view)
2409  method content = vbox1
2410  method compute = (assert false : unit)
2411 end
2412 ;;
2413
2414 let empty_page = new empty_page;;
2415
2416 class notebook =
2417 object(self)
2418  val notebook = GPack.notebook ()
2419  val pages = ref []
2420  val mutable skip_switch_page_event = false
2421  val mutable empty = true
2422  method notebook = notebook
2423  method add_page n =
2424   let new_page = new page () in
2425    empty <- false ;
2426    pages := !pages @ [n,lazy (setgoal n),new_page] ;
2427    notebook#append_page
2428     ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce)
2429     new_page#content#coerce
2430  method remove_all_pages ~skip_switch_page_event:skip =
2431   if empty then
2432    notebook#remove_page 0 (* let's remove the empty page *)
2433   else
2434    List.iter (function _ -> notebook#remove_page 0) !pages ;
2435   pages := [] ;
2436   skip_switch_page_event <- skip
2437  method set_current_page ~may_skip_switch_page_event n =
2438   let (_,_,page) = List.find (function (m,_,_) -> m=n) !pages in
2439    let new_page = notebook#page_num page#content#coerce in
2440     if may_skip_switch_page_event && new_page <> notebook#current_page then
2441      skip_switch_page_event <- true ;
2442     notebook#goto_page new_page
2443  method set_empty_page =
2444   empty <- true ;
2445   pages := [] ;
2446   notebook#append_page
2447    ~tab_label:((GMisc.label ~text:"No proof in progress" ())#coerce)
2448    empty_page#content#coerce
2449  method proofw =
2450   let (_,_,page) = List.nth !pages notebook#current_page in
2451    page#proofw
2452  initializer
2453   ignore
2454    (notebook#connect#switch_page
2455     (function i ->
2456       let skip = skip_switch_page_event in
2457        skip_switch_page_event <- false ;
2458        if not skip then
2459         try
2460          let (metano,setgoal,page) = List.nth !pages i in
2461           ProofEngine.goal := Some metano ;
2462           Lazy.force (page#compute) ;
2463           Lazy.force setgoal
2464         with _ -> ()
2465     ))
2466 end
2467 ;;
2468
2469 (* Main window *)
2470
2471 class rendering_window output (notebook : notebook) =
2472  let scratch_window = new scratch_window in
2473  let window =
2474   GWindow.window ~title:"MathML viewer" ~border_width:0
2475    ~allow_shrink:false () in
2476  let vbox_for_menu = GPack.vbox ~packing:window#add () in
2477  (* menus *)
2478  let handle_box = GBin.handle_box ~border_width:2
2479   ~packing:(vbox_for_menu#pack ~padding:0) () in
2480  let menubar = GMenu.menu_bar ~packing:handle_box#add () in
2481  let factory0 = new GMenu.factory menubar in
2482  let accel_group = factory0#accel_group in
2483  (* file menu *)
2484  let file_menu = factory0#add_submenu "File" in
2485  let factory1 = new GMenu.factory file_menu ~accel_group in
2486  let export_to_postscript_menu_item =
2487   begin
2488    let _ =
2489     factory1#add_item "New Proof or Definition..." ~key:GdkKeysyms._N
2490      ~callback:new_proof
2491    in
2492    let reopen_menu_item =
2493     factory1#add_item "Reopen a Finished Proof..." ~key:GdkKeysyms._R
2494      ~callback:open_
2495    in
2496    let qed_menu_item =
2497     factory1#add_item "Qed" ~key:GdkKeysyms._E ~callback:qed in
2498    ignore (factory1#add_separator ()) ;
2499    ignore
2500     (factory1#add_item "Load Unfinished Proof..." ~key:GdkKeysyms._L
2501       ~callback:load) ;
2502    let save_menu_item =
2503     factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S ~callback:save
2504    in
2505    ignore
2506     (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b);
2507    ignore (!save_set_sensitive false);
2508    ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b);
2509    ignore (!qed_set_sensitive false);
2510    ignore (factory1#add_separator ()) ;
2511    let export_to_postscript_menu_item =
2512     factory1#add_item "Export to PostScript..."
2513      ~callback:(export_to_postscript output) in
2514    ignore (factory1#add_separator ()) ;
2515    ignore
2516     (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) ;
2517    export_to_postscript_menu_item
2518   end in
2519  (* edit menu *)
2520  let edit_menu = factory0#add_submenu "Edit Current Proof" in
2521  let factory2 = new GMenu.factory edit_menu ~accel_group in
2522  let focus_and_proveit_set_sensitive = ref (function _ -> assert false) in
2523  let proveit_menu_item =
2524   factory2#add_item "Prove It" ~key:GdkKeysyms._I
2525    ~callback:(function () -> proveit ();!focus_and_proveit_set_sensitive false)
2526  in
2527  let focus_menu_item =
2528   factory2#add_item "Focus" ~key:GdkKeysyms._F
2529    ~callback:(function () -> focus () ; !focus_and_proveit_set_sensitive false)
2530  in
2531  let _ =
2532   focus_and_proveit_set_sensitive :=
2533    function b ->
2534     proveit_menu_item#misc#set_sensitive b ;
2535     focus_menu_item#misc#set_sensitive b
2536  in
2537  let _ = !focus_and_proveit_set_sensitive false in
2538  (* edit term menu *)
2539  let edit_term_menu = factory0#add_submenu "Edit Term" in
2540  let factory5 = new GMenu.factory edit_term_menu ~accel_group in
2541  let check_menu_item =
2542   factory5#add_item "Check Term" ~key:GdkKeysyms._C
2543    ~callback:(check scratch_window) in
2544  let _ = check_menu_item#misc#set_sensitive false in
2545  (* search menu *)
2546  let settings_menu = factory0#add_submenu "Search" in
2547  let factory4 = new GMenu.factory settings_menu ~accel_group in
2548  let _ =
2549   factory4#add_item "Locate..." ~key:GdkKeysyms._T
2550    ~callback:locate in
2551  let show_menu_item =
2552   factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show
2553  in
2554  (* settings menu *)
2555  let settings_menu = factory0#add_submenu "Settings" in
2556  let factory3 = new GMenu.factory settings_menu ~accel_group in
2557  let _ =
2558   factory3#add_item "Edit Aliases" ~key:GdkKeysyms._A
2559    ~callback:edit_aliases in
2560  let _ = factory3#add_separator () in
2561  let _ =
2562   factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P
2563    ~callback:(function _ -> (settings_window ())#show ()) in
2564  (* accel group *)
2565  let _ = window#add_accel_group accel_group in
2566  (* end of menus *)
2567  let hbox0 =
2568   GPack.hbox
2569    ~packing:(vbox_for_menu#pack ~expand:true ~fill:true ~padding:5) () in
2570  let vbox =
2571   GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
2572  let scrolled_window0 =
2573   GBin.scrolled_window ~border_width:10
2574    ~packing:(vbox#pack ~expand:true ~padding:5) () in
2575  let _ = scrolled_window0#add output#coerce in
2576  let frame =
2577   GBin.frame ~label:"Insert Term"
2578    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2579  let scrolled_window1 =
2580   GBin.scrolled_window ~border_width:5
2581    ~packing:frame#add () in
2582  let inputt =
2583   new term_editor ~width:400 ~height:100 ~packing:scrolled_window1#add ()
2584    ~isnotempty_callback:check_menu_item#misc#set_sensitive in
2585  let vboxl =
2586   GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
2587  let _ =
2588   vboxl#pack ~expand:true ~fill:true ~padding:5 notebook#notebook#coerce in
2589  let frame =
2590   GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
2591  in
2592  let outputhtml =
2593   GHtml.xmhtml
2594    ~source:"<html><body bgColor=\"white\"></body></html>"
2595    ~width:400 ~height: 100
2596    ~border_width:20
2597    ~packing:frame#add
2598    ~show:true () in
2599 object
2600  method outputhtml = outputhtml
2601  method inputt = inputt
2602  method output = (output : GMathView.math_view)
2603  method notebook = notebook
2604  method show = window#show
2605  initializer
2606   notebook#set_empty_page ;
2607   export_to_postscript_menu_item#misc#set_sensitive false ;
2608   check_term := (check_term_in_scratch scratch_window) ;
2609
2610   (* signal handlers here *)
2611   ignore(output#connect#selection_changed
2612    (function elem ->
2613      choose_selection output elem ;
2614      !focus_and_proveit_set_sensitive true
2615    )) ;
2616   ignore (output#connect#clicked (show_in_show_window_callback output)) ;
2617   let settings_window = new settings_window output scrolled_window0
2618    export_to_postscript_menu_item (choose_selection output) in
2619   set_settings_window settings_window ;
2620   set_outputhtml outputhtml ;
2621   ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
2622   Logger.log_callback :=
2623    (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
2624 end;;
2625
2626 (* MAIN *)
2627
2628 let initialize_everything () =
2629  let module U = Unix in
2630   let output = GMathView.math_view ~width:350 ~height:280 () in
2631   let notebook = new notebook in
2632    let rendering_window' = new rendering_window output notebook in
2633     set_rendering_window rendering_window' ;
2634     mml_of_cic_term_ref := mml_of_cic_term ;
2635     rendering_window'#show () ;
2636     GMain.Main.main ()
2637 ;;
2638
2639 let _ =
2640  if !usedb then
2641   begin
2642    Mqint.set_database Mqint.postgres_db ;
2643    (* Mqint.init "dbname=helm_mowgli" ; *)
2644    (* Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ; *)
2645    Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm" ;
2646   end ;
2647  ignore (GtkMain.Main.init ()) ;
2648  initialize_everything () ;
2649  if !usedb then Mqint.close ();
2650 ;;