helm/gTopLevel/gTopLevel.ml

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