helm/gTopLevel/gTopLevel.ml

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