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