helm/gTopLevel/gTopLevel.ml

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