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