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" ~border_width:2 () in
1337  let vbox = GPack.vbox ~packing:window#add () in
1338  let hbox =
1339   GPack.hbox ~border_width:0
1340    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1341  let _ =
1342   GMisc.label ~text:"Enter the URI for the new theorem or definition:"
1343    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1344  let uri_entry =
1345   GEdit.entry ~editable:true
1346    ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1347  let hbox1 =
1348   GPack.hbox ~border_width:0
1349    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1350  let _ =
1351   GMisc.label ~text:"Enter the theorem or definition type:"
1352    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1353  let scrolled_window =
1354   GBin.scrolled_window ~border_width:5
1355    ~packing:(vbox#pack ~expand:true ~padding:0) () in
1356  (* the content of the scrolled_window is moved below (see comment) *)
1357  let hbox =
1358   GPack.hbox ~border_width:0
1359    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1360  let okb =
1361   GButton.button ~label:"Ok"
1362    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1363  let _ = okb#misc#set_sensitive false in
1364  let cancelb =
1365   GButton.button ~label:"Cancel"
1366    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1367  (* moved here to have visibility of the ok button *)
1368  let newinputt =
1369   new term_editor ~width:400 ~height:100 ~packing:scrolled_window#add ()
1370    ~changed_callback:
1371     (function b ->
1372       non_empty_type := b ;
1373       okb#misc#set_sensitive (b && uri_entry#text <> ""))
1374  in
1375  let _ =
1376   newinputt#set_term inputt#get_as_string ;
1377   inputt#reset in
1378  let _ =
1379   uri_entry#connect#changed
1380    (function () ->
1381      okb#misc#set_sensitive (!non_empty_type && uri_entry#text <> ""))
1382  in
1383  ignore (window#connect#destroy GMain.Main.quit) ;
1384  ignore (cancelb#connect#clicked window#destroy) ;
1385  ignore
1386   (okb#connect#clicked
1387     (function () ->
1388       chosen := true ;
1389       try
1390        let parsed = newinputt#get_term [] [] in
1391        let uristr = "cic:" ^ uri_entry#text in
1392        let uri = UriManager.uri_of_string uristr in
1393         if String.sub uristr (String.length uristr - 4) 4 <> ".con" then
1394          raise NotAUriToAConstant
1395         else
1396          begin
1397           try
1398            ignore (Getter.resolve uri) ;
1399            raise UriAlreadyInUse
1400           with
1401            Getter.Unresolved ->
1402             get_parsed := (function () -> parsed) ;
1403             get_uri := (function () -> uri) ;
1404             window#destroy ()
1405          end
1406       with
1407        e ->
1408         output_html outputhtml
1409          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1410   )) ;
1411  window#show () ;
1412  GMain.Main.main () ;
1413  if !chosen then
1414   try
1415    let dom,mk_metasenv_and_expr = !get_parsed () in
1416     let metasenv,expr =
1417      disambiguate_input [] [] dom mk_metasenv_and_expr
1418     in
1419      let _  = CicTypeChecker.type_of_aux' metasenv [] expr in
1420       ProofEngine.proof :=
1421        Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
1422       ProofEngine.goal := Some 1 ;
1423       refresh_sequent notebook ;
1424       refresh_proof output ;
1425       !save_set_sensitive true ;
1426       inputt#reset
1427   with
1428      RefreshSequentException e ->
1429       output_html outputhtml
1430        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1431         "sequent: " ^ Printexc.to_string e ^ "</h1>")
1432    | RefreshProofException e ->
1433       output_html outputhtml
1434        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1435         "proof: " ^ Printexc.to_string e ^ "</h1>")
1436    | e ->
1437       output_html outputhtml
1438        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1439 ;;
1440
1441 let check_term_in_scratch scratch_window metasenv context expr =
1442  try
1443   let ty  = CicTypeChecker.type_of_aux' metasenv context expr in
1444    let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
1445 prerr_endline ("### " ^ CicPp.ppterm expr ^ " ==> " ^ CicPp.ppterm ty) ;
1446     scratch_window#show () ;
1447     scratch_window#mmlwidget#load_tree ~dom:mml
1448  with
1449   e ->
1450    print_endline ("? " ^ CicPp.ppterm expr) ;
1451    raise e
1452 ;;
1453
1454 let check scratch_window () =
1455  let inputt = ((rendering_window ())#inputt : term_editor) in
1456  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1457   let metasenv =
1458    match !ProofEngine.proof with
1459       None -> []
1460     | Some (_,metasenv,_,_) -> metasenv
1461   in
1462   let context,names_context =
1463    let context =
1464     match !ProofEngine.goal with
1465        None -> []
1466      | Some metano ->
1467         let (_,canonical_context,_) =
1468          List.find (function (m,_,_) -> m=metano) metasenv
1469         in
1470          canonical_context
1471    in
1472     context,
1473     List.map
1474      (function
1475          Some (n,_) -> Some n
1476        | None -> None
1477      ) context
1478   in
1479    try
1480     let dom,mk_metasenv_and_expr = inputt#get_term names_context metasenv in
1481      let (metasenv',expr) =
1482       disambiguate_input context metasenv dom mk_metasenv_and_expr
1483      in
1484       check_term_in_scratch scratch_window metasenv' context expr
1485    with
1486     e ->
1487      output_html outputhtml
1488       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1489 ;;
1490
1491
1492 (***********************)
1493 (*       TACTICS       *)
1494 (***********************)
1495
1496 let call_tactic tactic () =
1497  let notebook = (rendering_window ())#notebook in
1498  let output = ((rendering_window ())#output : GMathView.math_view) in
1499  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1500  let savedproof = !ProofEngine.proof in
1501  let savedgoal  = !ProofEngine.goal in
1502   begin
1503    try
1504     tactic () ;
1505     refresh_sequent notebook ;
1506     refresh_proof output
1507    with
1508       RefreshSequentException e ->
1509        output_html outputhtml
1510         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1511          "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1512        ProofEngine.proof := savedproof ;
1513        ProofEngine.goal := savedgoal ;
1514        refresh_sequent notebook
1515     | RefreshProofException e ->
1516        output_html outputhtml
1517         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1518          "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1519        ProofEngine.proof := savedproof ;
1520        ProofEngine.goal := savedgoal ;
1521        refresh_sequent notebook ;
1522        refresh_proof output
1523     | e ->
1524        output_html outputhtml
1525         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1526        ProofEngine.proof := savedproof ;
1527        ProofEngine.goal := savedgoal ;
1528   end
1529 ;;
1530
1531 let call_tactic_with_input tactic () =
1532  let notebook = (rendering_window ())#notebook in
1533  let output = ((rendering_window ())#output : GMathView.math_view) in
1534  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1535  let inputt = ((rendering_window ())#inputt : term_editor) in
1536  let savedproof = !ProofEngine.proof in
1537  let savedgoal  = !ProofEngine.goal in
1538   let uri,metasenv,bo,ty =
1539    match !ProofEngine.proof with
1540       None -> assert false
1541     | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
1542   in
1543    let canonical_context =
1544     match !ProofEngine.goal with
1545        None -> assert false
1546      | Some metano ->
1547         let (_,canonical_context,_) =
1548          List.find (function (m,_,_) -> m=metano) metasenv
1549         in
1550          canonical_context
1551    in
1552    let context =
1553     List.map
1554      (function
1555          Some (n,_) -> Some n
1556        | None -> None
1557      ) canonical_context
1558    in
1559     try
1560      let dom,mk_metasenv_and_expr = inputt#get_term context metasenv in
1561       let (metasenv',expr) =
1562        disambiguate_input canonical_context metasenv dom mk_metasenv_and_expr
1563       in
1564        ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
1565        tactic expr ;
1566        refresh_sequent notebook ;
1567        refresh_proof output ;
1568        inputt#reset
1569     with
1570        RefreshSequentException e ->
1571         output_html outputhtml
1572          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1573           "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1574         ProofEngine.proof := savedproof ;
1575         ProofEngine.goal := savedgoal ;
1576         refresh_sequent notebook
1577      | RefreshProofException e ->
1578         output_html outputhtml
1579          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1580           "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1581         ProofEngine.proof := savedproof ;
1582         ProofEngine.goal := savedgoal ;
1583         refresh_sequent notebook ;
1584         refresh_proof output
1585      | e ->
1586         output_html outputhtml
1587          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1588         ProofEngine.proof := savedproof ;
1589         ProofEngine.goal := savedgoal ;
1590 ;;
1591
1592 let call_tactic_with_goal_input tactic () =
1593  let module L = LogicalOperations in
1594  let module G = Gdome in
1595   let notebook = (rendering_window ())#notebook in
1596   let output = ((rendering_window ())#output : GMathView.math_view) in
1597   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1598   let savedproof = !ProofEngine.proof in
1599   let savedgoal  = !ProofEngine.goal in
1600    match notebook#proofw#get_selection with
1601      Some node ->
1602       let xpath =
1603        ((node : Gdome.element)#getAttributeNS
1604          ~namespaceURI:helmns
1605          ~localName:(G.domString "xref"))#to_string
1606       in
1607        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1608        else
1609         begin
1610          try
1611           match !current_goal_infos with
1612              Some (ids_to_terms, ids_to_father_ids,_) ->
1613               let id = xpath in
1614                tactic (Hashtbl.find ids_to_terms id) ;
1615                refresh_sequent notebook ;
1616                refresh_proof output
1617            | None -> assert false (* "ERROR: No current term!!!" *)
1618          with
1619             RefreshSequentException e ->
1620              output_html outputhtml
1621               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1622                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1623              ProofEngine.proof := savedproof ;
1624              ProofEngine.goal := savedgoal ;
1625              refresh_sequent notebook
1626           | RefreshProofException e ->
1627              output_html outputhtml
1628               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1629                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1630              ProofEngine.proof := savedproof ;
1631              ProofEngine.goal := savedgoal ;
1632              refresh_sequent notebook ;
1633              refresh_proof output
1634           | e ->
1635              output_html outputhtml
1636               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1637              ProofEngine.proof := savedproof ;
1638              ProofEngine.goal := savedgoal ;
1639         end
1640    | None ->
1641       output_html outputhtml
1642        ("<h1 color=\"red\">No term selected</h1>")
1643 ;;
1644
1645 let call_tactic_with_input_and_goal_input tactic () =
1646  let module L = LogicalOperations in
1647  let module G = Gdome in
1648   let notebook = (rendering_window ())#notebook in
1649   let output = ((rendering_window ())#output : GMathView.math_view) in
1650   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1651   let inputt = ((rendering_window ())#inputt : term_editor) in
1652   let savedproof = !ProofEngine.proof in
1653   let savedgoal  = !ProofEngine.goal in
1654    match notebook#proofw#get_selection with
1655      Some node ->
1656       let xpath =
1657        ((node : Gdome.element)#getAttributeNS
1658          ~namespaceURI:helmns
1659          ~localName:(G.domString "xref"))#to_string
1660       in
1661        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1662        else
1663         begin
1664          try
1665           match !current_goal_infos with
1666              Some (ids_to_terms, ids_to_father_ids,_) ->
1667               let id = xpath in
1668                let uri,metasenv,bo,ty =
1669                 match !ProofEngine.proof with
1670                    None -> assert false
1671                  | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
1672                in
1673                 let canonical_context =
1674                  match !ProofEngine.goal with
1675                     None -> assert false
1676                   | Some metano ->
1677                      let (_,canonical_context,_) =
1678                       List.find (function (m,_,_) -> m=metano) metasenv
1679                      in
1680                       canonical_context in
1681                 let context =
1682                  List.map
1683                   (function
1684                       Some (n,_) -> Some n
1685                     | None -> None
1686                   ) canonical_context
1687                 in
1688                  let dom,mk_metasenv_and_expr = inputt#get_term context metasenv
1689                  in
1690                   let (metasenv',expr) =
1691                    disambiguate_input canonical_context metasenv dom
1692                     mk_metasenv_and_expr
1693                   in
1694                    ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
1695                    tactic ~goal_input:(Hashtbl.find ids_to_terms id)
1696                     ~input:expr ;
1697                    refresh_sequent notebook ;
1698                    refresh_proof output ;
1699                    inputt#reset
1700            | None -> assert false (* "ERROR: No current term!!!" *)
1701          with
1702             RefreshSequentException e ->
1703              output_html outputhtml
1704               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1705                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1706              ProofEngine.proof := savedproof ;
1707              ProofEngine.goal := savedgoal ;
1708              refresh_sequent notebook
1709           | RefreshProofException e ->
1710              output_html outputhtml
1711               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1712                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1713              ProofEngine.proof := savedproof ;
1714              ProofEngine.goal := savedgoal ;
1715              refresh_sequent notebook ;
1716              refresh_proof output
1717           | e ->
1718              output_html outputhtml
1719               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1720              ProofEngine.proof := savedproof ;
1721              ProofEngine.goal := savedgoal ;
1722         end
1723    | None ->
1724       output_html outputhtml
1725        ("<h1 color=\"red\">No term selected</h1>")
1726 ;;
1727
1728 let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
1729  let module L = LogicalOperations in
1730  let module G = Gdome in
1731   let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in
1732   let outputhtml = (scratch_window#outputhtml : GHtml.xmhtml) in
1733   let savedproof = !ProofEngine.proof in
1734   let savedgoal  = !ProofEngine.goal in
1735    match mmlwidget#get_selection with
1736      Some node ->
1737       let xpath =
1738        ((node : Gdome.element)#getAttributeNS
1739          ~namespaceURI:helmns
1740          ~localName:(G.domString "xref"))#to_string
1741       in
1742        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1743        else
1744         begin
1745          try
1746           match !current_scratch_infos with
1747              (* term is the whole goal in the scratch_area *)
1748              Some (term,ids_to_terms, ids_to_father_ids,_) ->
1749               let id = xpath in
1750                let expr = tactic term (Hashtbl.find ids_to_terms id) in
1751                 let mml = mml_of_cic_term 111 expr in
1752                  scratch_window#show () ;
1753                  scratch_window#mmlwidget#load_tree ~dom:mml
1754            | None -> assert false (* "ERROR: No current term!!!" *)
1755          with
1756           e ->
1757            output_html outputhtml
1758             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1759         end
1760    | None ->
1761       output_html outputhtml
1762        ("<h1 color=\"red\">No term selected</h1>")
1763 ;;
1764
1765 let call_tactic_with_hypothesis_input tactic () =
1766  let module L = LogicalOperations in
1767  let module G = Gdome in
1768   let notebook = (rendering_window ())#notebook in
1769   let output = ((rendering_window ())#output : GMathView.math_view) in
1770   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1771   let savedproof = !ProofEngine.proof in
1772   let savedgoal  = !ProofEngine.goal in
1773    match notebook#proofw#get_selection with
1774      Some node ->
1775       let xpath =
1776        ((node : Gdome.element)#getAttributeNS
1777          ~namespaceURI:helmns
1778          ~localName:(G.domString "xref"))#to_string
1779       in
1780        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1781        else
1782         begin
1783          try
1784           match !current_goal_infos with
1785              Some (_,_,ids_to_hypotheses) ->
1786               let id = xpath in
1787                tactic (Hashtbl.find ids_to_hypotheses id) ;
1788                refresh_sequent notebook ;
1789                refresh_proof output
1790            | None -> assert false (* "ERROR: No current term!!!" *)
1791          with
1792             RefreshSequentException e ->
1793              output_html outputhtml
1794               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1795                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1796              ProofEngine.proof := savedproof ;
1797              ProofEngine.goal := savedgoal ;
1798              refresh_sequent notebook
1799           | RefreshProofException e ->
1800              output_html outputhtml
1801               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1802                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1803              ProofEngine.proof := savedproof ;
1804              ProofEngine.goal := savedgoal ;
1805              refresh_sequent notebook ;
1806              refresh_proof output
1807           | e ->
1808              output_html outputhtml
1809               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1810              ProofEngine.proof := savedproof ;
1811              ProofEngine.goal := savedgoal ;
1812         end
1813    | None ->
1814       output_html outputhtml
1815        ("<h1 color=\"red\">No term selected</h1>")
1816 ;;
1817
1818
1819 let intros = call_tactic ProofEngine.intros;;
1820 let exact = call_tactic_with_input ProofEngine.exact;;
1821 let apply = call_tactic_with_input ProofEngine.apply;;
1822 let elimsimplintros = call_tactic_with_input ProofEngine.elim_simpl_intros;;
1823 let elimtype = call_tactic_with_input ProofEngine.elim_type;;
1824 let whd = call_tactic_with_goal_input ProofEngine.whd;;
1825 let reduce = call_tactic_with_goal_input ProofEngine.reduce;;
1826 let simpl = call_tactic_with_goal_input ProofEngine.simpl;;
1827 let fold = call_tactic_with_input ProofEngine.fold;;
1828 let cut = call_tactic_with_input ProofEngine.cut;;
1829 let change = call_tactic_with_input_and_goal_input ProofEngine.change;;
1830 let letin = call_tactic_with_input ProofEngine.letin;;
1831 let ring = call_tactic ProofEngine.ring;;
1832 let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody;;
1833 let clear = call_tactic_with_hypothesis_input ProofEngine.clear;;
1834 let fourier = call_tactic ProofEngine.fourier;;
1835 let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl;;
1836 let reflexivity = call_tactic ProofEngine.reflexivity;;
1837 let symmetry = call_tactic ProofEngine.symmetry;;
1838 let transitivity = call_tactic_with_input ProofEngine.transitivity;;
1839 let left = call_tactic ProofEngine.left;;
1840 let right = call_tactic ProofEngine.right;;
1841 let assumption = call_tactic ProofEngine.assumption;;
1842
1843 let whd_in_scratch scratch_window =
1844  call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
1845   scratch_window
1846 ;;
1847 let reduce_in_scratch scratch_window =
1848  call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch
1849   scratch_window
1850 ;;
1851 let simpl_in_scratch scratch_window =
1852  call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch
1853   scratch_window
1854 ;;
1855
1856
1857
1858 (**********************)
1859 (*   END OF TACTICS   *)
1860 (**********************)
1861
1862
1863 let show () =
1864  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1865   try
1866    show_in_show_window (input_or_locate_uri ~title:"Show")
1867   with
1868    e ->
1869     output_html outputhtml
1870      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1871 ;;
1872
1873 exception NotADefinition;;
1874
1875 let open_ () =
1876  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1877  let output = ((rendering_window ())#output : GMathView.math_view) in
1878  let notebook = (rendering_window ())#notebook in
1879    try
1880     let uri = input_or_locate_uri ~title:"Open" in
1881      CicTypeChecker.typecheck uri ;
1882      let metasenv,bo,ty =
1883       match CicEnvironment.get_cooked_obj uri with
1884          Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
1885        | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
1886        | Cic.Constant _
1887        | Cic.Variable _
1888        | Cic.InductiveDefinition _ -> raise NotADefinition
1889      in
1890       ProofEngine.proof :=
1891        Some (uri, metasenv, bo, ty) ;
1892       ProofEngine.goal := None ;
1893       refresh_sequent notebook ;
1894       refresh_proof output
1895    with
1896       RefreshSequentException e ->
1897        output_html outputhtml
1898         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1899          "sequent: " ^ Printexc.to_string e ^ "</h1>")
1900     | RefreshProofException e ->
1901        output_html outputhtml
1902         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1903          "proof: " ^ Printexc.to_string e ^ "</h1>")
1904     | e ->
1905        output_html outputhtml
1906         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1907 ;;
1908
1909
1910 let searchPattern () =
1911  let inputt = ((rendering_window ())#inputt : term_editor) in
1912  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1913   try
1914    let rec get_level ?(last_invalid=false) () =
1915     match
1916      GToolbox.input_string
1917       ~title:"Insert the strictness parameter for the query:"
1918       ((if last_invalid then
1919          "Invalid input (must be a non-negative natural number). Insert again "
1920         else
1921          "Insert "
1922        ) ^ "the strictness parameter for the query:")
1923     with
1924        None -> raise NoChoice
1925      | Some n ->
1926         try
1927          int_of_string n
1928         with
1929          _ -> get_level ~last_invalid:true ()
1930    in
1931     let level = get_level () in
1932     let metasenv =
1933      match !ProofEngine.proof with
1934         None -> assert false
1935       | Some (_,metasenv,_,_) -> metasenv
1936     in
1937      match !ProofEngine.goal with
1938         None -> ()
1939       | Some metano ->
1940          let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
1941           let result = MQueryGenerator.searchPattern metasenv ey ty level in
1942           let uris =
1943            List.map
1944             (function uri,_ ->
1945               wrong_xpointer_format_from_wrong_xpointer_format' uri
1946             ) result in
1947           let html =
1948            " <h1>Backward Query: </h1>" ^
1949            " <h2>Levels: </h2> " ^
1950            MQueryGenerator.string_of_levels
1951             (MQueryGenerator.levels_of_term metasenv ey ty) "<br>" ^
1952            " <pre>" ^ get_last_query result ^ "</pre>"
1953           in
1954            output_html outputhtml html ;
1955            let uris',exc =
1956             let rec filter_out =
1957              function
1958                 [] -> [],""
1959               | uri::tl ->
1960                  let tl',exc = filter_out tl in
1961                   try
1962                    if
1963                     ProofEngine.can_apply
1964                      (term_of_cic_textual_parser_uri
1965                       (cic_textual_parser_uri_of_string uri))
1966                    then
1967                     uri::tl',exc
1968                    else
1969                     tl',exc
1970                   with
1971                    e ->
1972                     let exc' =
1973                      "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
1974                       uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
1975                     in
1976                      tl',exc'
1977             in
1978              filter_out uris
1979            in
1980             let html' =
1981              " <h1>Objects that can actually be applied: </h1> " ^
1982              String.concat "<br>" uris' ^ exc ^
1983              " <h1>Number of false matches: " ^
1984               string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
1985              " <h1>Number of good matches: " ^
1986               string_of_int (List.length uris') ^ "</h1>"
1987             in
1988              output_html outputhtml html' ;
1989              let uri' =
1990               user_uri_choice ~title:"Ambiguous input."
1991               ~msg:
1992                 "Many lemmas can be successfully applied. Please, choose one:"
1993                uris'
1994              in
1995               inputt#set_term uri' ;
1996               apply ()
1997   with
1998    e ->
1999     output_html outputhtml
2000      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2001 ;;
2002
2003 let choose_selection
2004      (mmlwidget : GMathView.math_view) (element : Gdome.element option)
2005 =
2006  let module G = Gdome in
2007   let rec aux element =
2008    if element#hasAttributeNS
2009        ~namespaceURI:helmns
2010        ~localName:(G.domString "xref")
2011    then
2012      mmlwidget#set_selection (Some element)
2013    else
2014       match element#get_parentNode with
2015          None -> assert false
2016        (*CSC: OCAML DIVERGES!
2017        | Some p -> aux (new G.element_of_node p)
2018        *)
2019        | Some p -> aux (new Gdome.element_of_node p)
2020   in
2021    match element with
2022      Some x -> aux x
2023    | None   -> mmlwidget#set_selection None
2024 ;;
2025
2026 (* STUFF TO BUILD THE GTK INTERFACE *)
2027
2028 (* Stuff for the widget settings *)
2029
2030 let export_to_postscript (output : GMathView.math_view) =
2031  let lastdir = ref (Unix.getcwd ()) in
2032   function () ->
2033    match
2034     GToolbox.select_file ~title:"Export to PostScript"
2035      ~dir:lastdir ~filename:"screenshot.ps" ()
2036    with
2037       None -> ()
2038     | Some filename ->
2039        output#export_to_postscript ~filename:filename ();
2040 ;;
2041
2042 let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
2043  button_set_kerning button_set_transparency export_to_postscript_menu_item
2044  button_t1 ()
2045 =
2046  let is_set = button_t1#active in
2047   output#set_font_manager_type
2048    (if is_set then `font_manager_t1 else `font_manager_gtk) ;
2049   if is_set then
2050    begin
2051     button_set_anti_aliasing#misc#set_sensitive true ;
2052     button_set_kerning#misc#set_sensitive true ;
2053     button_set_transparency#misc#set_sensitive true ;
2054     export_to_postscript_menu_item#misc#set_sensitive true ;
2055    end
2056   else
2057    begin
2058     button_set_anti_aliasing#misc#set_sensitive false ;
2059     button_set_kerning#misc#set_sensitive false ;
2060     button_set_transparency#misc#set_sensitive false ;
2061     export_to_postscript_menu_item#misc#set_sensitive false ;
2062    end
2063 ;;
2064
2065 let set_anti_aliasing output button_set_anti_aliasing () =
2066  output#set_anti_aliasing button_set_anti_aliasing#active
2067 ;;
2068
2069 let set_kerning output button_set_kerning () =
2070  output#set_kerning button_set_kerning#active
2071 ;;
2072
2073 let set_transparency output button_set_transparency () =
2074  output#set_transparency button_set_transparency#active
2075 ;;
2076
2077 let changefont output font_size_spinb () =
2078  output#set_font_size font_size_spinb#value_as_int
2079 ;;
2080
2081 let set_log_verbosity output log_verbosity_spinb () =
2082  output#set_log_verbosity log_verbosity_spinb#value_as_int
2083 ;;
2084
2085 class settings_window (output : GMathView.math_view) sw
2086  export_to_postscript_menu_item selection_changed_callback
2087 =
2088  let settings_window = GWindow.window ~title:"GtkMathView settings" () in
2089  let vbox =
2090   GPack.vbox ~packing:settings_window#add () in
2091  let table =
2092   GPack.table
2093    ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
2094    ~border_width:5 ~packing:vbox#add () in
2095  let button_t1 =
2096   GButton.toggle_button ~label:"activate t1 fonts"
2097    ~packing:(table#attach ~left:0 ~top:0) () in
2098  let button_set_anti_aliasing =
2099   GButton.toggle_button ~label:"set_anti_aliasing"
2100    ~packing:(table#attach ~left:0 ~top:1) () in
2101  let button_set_kerning =
2102   GButton.toggle_button ~label:"set_kerning"
2103    ~packing:(table#attach ~left:1 ~top:1) () in
2104  let button_set_transparency =
2105   GButton.toggle_button ~label:"set_transparency"
2106    ~packing:(table#attach ~left:2 ~top:1) () in
2107  let table =
2108   GPack.table
2109    ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
2110    ~border_width:5 ~packing:vbox#add () in
2111  let font_size_label =
2112   GMisc.label ~text:"font size:"
2113    ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
2114  let font_size_spinb =
2115   let sadj =
2116    GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
2117   in
2118    GEdit.spin_button
2119     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
2120  let log_verbosity_label =
2121   GMisc.label ~text:"log verbosity:"
2122    ~packing:(table#attach ~left:0 ~top:1) () in
2123  let log_verbosity_spinb =
2124   let sadj =
2125    GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
2126   in
2127    GEdit.spin_button
2128     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
2129  let hbox =
2130   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2131  let closeb =
2132   GButton.button ~label:"Close"
2133    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2134 object(self)
2135  method show = settings_window#show
2136  initializer
2137   button_set_anti_aliasing#misc#set_sensitive false ;
2138   button_set_kerning#misc#set_sensitive false ;
2139   button_set_transparency#misc#set_sensitive false ;
2140   (* Signals connection *)
2141   ignore(button_t1#connect#clicked
2142    (activate_t1 output button_set_anti_aliasing button_set_kerning
2143     button_set_transparency export_to_postscript_menu_item button_t1)) ;
2144   ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
2145   ignore(button_set_anti_aliasing#connect#toggled
2146    (set_anti_aliasing output button_set_anti_aliasing));
2147   ignore(button_set_kerning#connect#toggled
2148    (set_kerning output button_set_kerning)) ;
2149   ignore(button_set_transparency#connect#toggled
2150    (set_transparency output button_set_transparency)) ;
2151   ignore(log_verbosity_spinb#connect#changed
2152    (set_log_verbosity output log_verbosity_spinb)) ;
2153   ignore(closeb#connect#clicked settings_window#misc#hide)
2154 end;;
2155
2156 (* Scratch window *)
2157
2158 class scratch_window outputhtml =
2159  let window =
2160   GWindow.window ~title:"MathML viewer" ~border_width:2 () in
2161  let vbox =
2162   GPack.vbox ~packing:window#add () in
2163  let hbox =
2164   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2165  let whdb =
2166   GButton.button ~label:"Whd"
2167    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2168  let reduceb =
2169   GButton.button ~label:"Reduce"
2170    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2171  let simplb =
2172   GButton.button ~label:"Simpl"
2173    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2174  let scrolled_window =
2175   GBin.scrolled_window ~border_width:10
2176    ~packing:(vbox#pack ~expand:true ~padding:5) () in
2177  let mmlwidget =
2178   GMathView.math_view
2179    ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
2180 object(self)
2181  method outputhtml = outputhtml
2182  method mmlwidget = mmlwidget
2183  method show () = window#misc#hide () ; window#show ()
2184  initializer
2185   ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
2186   ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
2187   ignore(whdb#connect#clicked (whd_in_scratch self)) ;
2188   ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
2189   ignore(simplb#connect#clicked (simpl_in_scratch self))
2190 end;;
2191
2192 class page () =
2193  let vbox1 = GPack.vbox () in
2194 object(self)
2195  val mutable proofw_ref = None
2196  val mutable compute_ref = None
2197  method proofw =
2198   Lazy.force self#compute ;
2199   match proofw_ref with
2200      None -> assert false
2201    | Some proofw -> proofw
2202  method content = vbox1
2203  method compute =
2204   match compute_ref with
2205      None -> assert false
2206    | Some compute -> compute
2207  initializer
2208   compute_ref <-
2209    Some (lazy (
2210    let scrolled_window1 =
2211     GBin.scrolled_window ~border_width:10
2212      ~packing:(vbox1#pack ~expand:true ~padding:5) () in
2213    let proofw =
2214     GMathView.math_view ~width:400 ~height:275
2215      ~packing:(scrolled_window1#add) () in
2216    let _ = proofw_ref <- Some proofw in
2217    let hbox3 =
2218     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
2219    let exactb =
2220     GButton.button ~label:"Exact"
2221      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2222    let introsb =
2223     GButton.button ~label:"Intros"
2224      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2225    let applyb =
2226     GButton.button ~label:"Apply"
2227      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2228    let elimsimplintrosb =
2229     GButton.button ~label:"ElimSimplIntros"
2230      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2231    let elimtypeb =
2232     GButton.button ~label:"ElimType"
2233      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2234    let whdb =
2235     GButton.button ~label:"Whd"
2236      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2237    let reduceb =
2238     GButton.button ~label:"Reduce"
2239      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2240    let simplb =
2241     GButton.button ~label:"Simpl"
2242      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2243    let foldb =
2244     GButton.button ~label:"Fold"
2245      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2246    let cutb =
2247     GButton.button ~label:"Cut"
2248      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2249    let hbox4 =
2250     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
2251    let changeb =
2252     GButton.button ~label:"Change"
2253      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2254    let letinb =
2255     GButton.button ~label:"Let ... In"
2256      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2257    let ringb =
2258     GButton.button ~label:"Ring"
2259      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2260    let clearbodyb =
2261     GButton.button ~label:"ClearBody"
2262      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2263    let clearb =
2264     GButton.button ~label:"Clear"
2265      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2266    let fourierb =
2267     GButton.button ~label:"Fourier"
2268      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2269    let rewritesimplb =
2270     GButton.button ~label:"RewriteSimpl ->"
2271      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2272    let reflexivityb =
2273     GButton.button ~label:"Reflexivity"
2274      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2275    let hbox5 =
2276     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
2277    let symmetryb =
2278     GButton.button ~label:"Symmetry"
2279      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2280    let transitivityb =
2281     GButton.button ~label:"Transitivity"
2282      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2283    let leftb =
2284     GButton.button ~label:"Left"
2285      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2286    let rightb =
2287     GButton.button ~label:"Right"
2288      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2289    let assumptionb =
2290     GButton.button ~label:"Assumption"
2291      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2292    let searchpatternb =
2293     GButton.button ~label:"SearchPattern_Apply"
2294      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2295    ignore(exactb#connect#clicked exact) ;
2296    ignore(applyb#connect#clicked apply) ;
2297    ignore(elimsimplintrosb#connect#clicked elimsimplintros) ;
2298    ignore(elimtypeb#connect#clicked elimtype) ;
2299    ignore(whdb#connect#clicked whd) ;
2300    ignore(reduceb#connect#clicked reduce) ;
2301    ignore(simplb#connect#clicked simpl) ;
2302    ignore(foldb#connect#clicked fold) ;
2303    ignore(cutb#connect#clicked cut) ;
2304    ignore(changeb#connect#clicked change) ;
2305    ignore(letinb#connect#clicked letin) ;
2306    ignore(ringb#connect#clicked ring) ;
2307    ignore(clearbodyb#connect#clicked clearbody) ;
2308    ignore(clearb#connect#clicked clear) ;
2309    ignore(fourierb#connect#clicked fourier) ;
2310    ignore(rewritesimplb#connect#clicked rewritesimpl) ;
2311    ignore(reflexivityb#connect#clicked reflexivity) ;
2312    ignore(symmetryb#connect#clicked symmetry) ;
2313    ignore(transitivityb#connect#clicked transitivity) ;
2314    ignore(leftb#connect#clicked left) ;
2315    ignore(rightb#connect#clicked right) ;
2316    ignore(assumptionb#connect#clicked assumption) ;
2317    ignore(introsb#connect#clicked intros) ;
2318    ignore(searchpatternb#connect#clicked searchPattern) ;
2319    ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
2320   ))
2321 end
2322 ;;
2323
2324 class empty_page =
2325  let vbox1 = GPack.vbox () in
2326  let scrolled_window1 =
2327   GBin.scrolled_window ~border_width:10
2328    ~packing:(vbox1#pack ~expand:true ~padding:5) () in
2329  let proofw =
2330   GMathView.math_view ~width:400 ~height:275
2331    ~packing:(scrolled_window1#add) () in
2332 object(self)
2333  method proofw = (assert false : GMathView.math_view)
2334  method content = vbox1
2335  method compute = (assert false : unit)
2336 end
2337 ;;
2338
2339 let empty_page = new empty_page;;
2340
2341 class notebook =
2342 object(self)
2343  val notebook = GPack.notebook ()
2344  val pages = ref []
2345  val mutable skip_switch_page_event = false
2346  val mutable empty = true
2347  method notebook = notebook
2348  method add_page n =
2349   let new_page = new page () in
2350    empty <- false ;
2351    pages := !pages @ [n,lazy (setgoal n),new_page] ;
2352    notebook#append_page
2353     ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce)
2354     new_page#content#coerce
2355  method remove_all_pages ~skip_switch_page_event:skip =
2356   if empty then
2357    notebook#remove_page 0 (* let's remove the empty page *)
2358   else
2359    List.iter (function _ -> notebook#remove_page 0) !pages ;
2360   pages := [] ;
2361   skip_switch_page_event <- skip
2362  method set_current_page ~may_skip_switch_page_event n =
2363   let (_,_,page) = List.find (function (m,_,_) -> m=n) !pages in
2364    let new_page = notebook#page_num page#content#coerce in
2365     if may_skip_switch_page_event && new_page <> notebook#current_page then
2366      skip_switch_page_event <- true ;
2367     notebook#goto_page new_page
2368  method set_empty_page =
2369   empty <- true ;
2370   pages := [] ;
2371   notebook#append_page
2372    ~tab_label:((GMisc.label ~text:"No proof in progress" ())#coerce)
2373    empty_page#content#coerce
2374  method proofw =
2375   let (_,_,page) = List.nth !pages notebook#current_page in
2376    page#proofw
2377  initializer
2378   ignore
2379    (notebook#connect#switch_page
2380     (function i ->
2381       let skip = skip_switch_page_event in
2382        skip_switch_page_event <- false ;
2383        if not skip then
2384         try
2385          let (metano,setgoal,page) = List.nth !pages i in
2386           ProofEngine.goal := Some metano ;
2387           Lazy.force (page#compute) ;
2388           Lazy.force setgoal
2389         with _ -> ()
2390     ))
2391 end
2392 ;;
2393
2394 (* Main window *)
2395
2396 class rendering_window output (notebook : notebook) =
2397  let window =
2398   GWindow.window ~title:"MathML viewer" ~border_width:2
2399    ~allow_shrink:false () in
2400  let vbox_for_menu = GPack.vbox ~packing:window#add () in
2401  (* menus *)
2402  let menubar = GMenu.menu_bar ~packing:vbox_for_menu#pack () in
2403  let factory0 = new GMenu.factory menubar in
2404  let accel_group = factory0#accel_group in
2405  (* file menu *)
2406  let file_menu = factory0#add_submenu "File" in
2407  let factory1 = new GMenu.factory file_menu ~accel_group in
2408  let export_to_postscript_menu_item =
2409   begin
2410    let _ =
2411     factory1#add_item "New Proof or Definition" ~key:GdkKeysyms._N
2412      ~callback:new_proof
2413    in
2414    let reopen_menu_item =
2415     factory1#add_item "Reopen a Finished Proof..." ~key:GdkKeysyms._R
2416      ~callback:open_
2417    in
2418    let qed_menu_item =
2419     factory1#add_item "Qed" ~key:GdkKeysyms._Q ~callback:qed in
2420    ignore (factory1#add_separator ()) ;
2421    ignore
2422     (factory1#add_item "Load Unfinished Proof" ~key:GdkKeysyms._L
2423       ~callback:load) ;
2424    let save_menu_item =
2425     factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S ~callback:save
2426    in
2427    ignore
2428     (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b);
2429    ignore (!save_set_sensitive false);
2430    ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b);
2431    ignore (!qed_set_sensitive false);
2432    ignore (factory1#add_separator ()) ;
2433    let export_to_postscript_menu_item =
2434     factory1#add_item "Export to PostScript..." ~key:GdkKeysyms._E
2435      ~callback:(export_to_postscript output) in
2436    ignore (factory1#add_separator ()) ;
2437    ignore
2438     (factory1#add_item "Exit" ~key:GdkKeysyms._C ~callback:GMain.Main.quit) ;
2439    export_to_postscript_menu_item
2440   end in
2441  (* edit menu *)
2442  let edit_menu = factory0#add_submenu "Edit current proof" in
2443  let factory2 = new GMenu.factory edit_menu ~accel_group in
2444  let focus_and_proveit_set_sensitive = ref (function _ -> assert false) in
2445  let proveit_menu_item =
2446   factory2#add_item "Prove It" ~key:GdkKeysyms._I
2447    ~callback:(function () -> proveit ();!focus_and_proveit_set_sensitive false)
2448  in
2449  let focus_menu_item =
2450   factory2#add_item "Focus" ~key:GdkKeysyms._F
2451    ~callback:(function () -> focus () ; !focus_and_proveit_set_sensitive false)
2452  in
2453  let _ =
2454   focus_and_proveit_set_sensitive :=
2455    function b ->
2456     proveit_menu_item#misc#set_sensitive b ;
2457     focus_menu_item#misc#set_sensitive b
2458  in
2459  let _ = !focus_and_proveit_set_sensitive false in
2460  (* search menu *)
2461  let settings_menu = factory0#add_submenu "Search" in
2462  let factory4 = new GMenu.factory settings_menu ~accel_group in
2463  let _ =
2464   factory4#add_item "Locate..." ~key:GdkKeysyms._T
2465    ~callback:locate in
2466  let show_menu_item =
2467   factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show
2468  in
2469  (* settings menu *)
2470  let settings_menu = factory0#add_submenu "Settings" in
2471  let factory3 = new GMenu.factory settings_menu ~accel_group in
2472  let _ =
2473   factory3#add_item "Edit Aliases" ~key:GdkKeysyms._A
2474    ~callback:edit_aliases in
2475  let _ = factory3#add_separator () in
2476  let _ =
2477   factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P
2478    ~callback:(function _ -> (settings_window ())#show ()) in
2479  (* accel group *)
2480  let _ = window#add_accel_group accel_group in
2481  (* end of menus *)
2482  let hbox0 =
2483   GPack.hbox
2484    ~packing:(vbox_for_menu#pack ~expand:true ~fill:true ~padding:5) () in
2485  let vbox =
2486   GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
2487  let scrolled_window0 =
2488   GBin.scrolled_window ~border_width:10
2489    ~packing:(vbox#pack ~expand:true ~padding:5) () in
2490  let _ = scrolled_window0#add output#coerce in
2491  let frame =
2492   GBin.frame ~label:"Term input"
2493    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2494  let vbox' =
2495   GPack.vbox ~packing:frame#add () in
2496  let hbox4 =
2497   GPack.hbox ~border_width:5 ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2498  let checkb =
2499   GButton.button ~label:"Check"
2500    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2501  let scrolled_window1 =
2502   GBin.scrolled_window ~border_width:5
2503    ~packing:(vbox'#pack ~expand:true ~padding:0) () in
2504  let inputt =
2505   new term_editor ~width:400 ~height:100 ~packing:scrolled_window1#add () in
2506  let vboxl =
2507   GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
2508  let _ =
2509   vboxl#pack ~expand:true ~fill:true ~padding:5 notebook#notebook#coerce in
2510  let frame =
2511   GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
2512  in
2513  let outputhtml =
2514   GHtml.xmhtml
2515    ~source:"<html><body bgColor=\"white\"></body></html>"
2516    ~width:400 ~height: 100
2517    ~border_width:20
2518    ~packing:frame#add
2519    ~show:true () in
2520  let scratch_window = new scratch_window outputhtml in
2521 object
2522  method outputhtml = outputhtml
2523  method inputt = inputt
2524  method output = (output : GMathView.math_view)
2525  method notebook = notebook
2526  method show = window#show
2527  initializer
2528   notebook#set_empty_page ;
2529   export_to_postscript_menu_item#misc#set_sensitive false ;
2530   check_term := (check_term_in_scratch scratch_window) ;
2531
2532   (* signal handlers here *)
2533   ignore(output#connect#selection_changed
2534    (function elem ->
2535      choose_selection output elem ;
2536      !focus_and_proveit_set_sensitive true
2537    )) ;
2538   ignore (output#connect#clicked (show_in_show_window_callback output)) ;
2539   let settings_window = new settings_window output scrolled_window0
2540    export_to_postscript_menu_item (choose_selection output) in
2541   set_settings_window settings_window ;
2542   set_outputhtml outputhtml ;
2543   ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
2544   ignore(checkb#connect#clicked (check scratch_window)) ;
2545   Logger.log_callback :=
2546    (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
2547 end;;
2548
2549 (* MAIN *)
2550
2551 let initialize_everything () =
2552  let module U = Unix in
2553   let output = GMathView.math_view ~width:350 ~height:280 () in
2554   let notebook = new notebook in
2555    let rendering_window' = new rendering_window output notebook in
2556     set_rendering_window rendering_window' ;
2557     mml_of_cic_term_ref := mml_of_cic_term ;
2558     rendering_window'#show () ;
2559     GMain.Main.main ()
2560 ;;
2561
2562 let _ =
2563  if !usedb then
2564  Mqint.init "dbname=helm_mowgli" ;
2565 (* Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ; *)
2566  ignore (GtkMain.Main.init ()) ;
2567  initialize_everything () ;
2568  if !usedb then Mqint.close ();
2569 ;;