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