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