helm/gTopLevel/gTopLevel.ml

   1 (* Copyright (C) 2000, 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 (* GLOBAL CONSTANTS *)
  37
  38 let helmns = Gdome.domString "http://www.cs.unibo.it/helm";;
  39
  40 let htmlheader =
  41  "<html>" ^
  42  " <body bgColor=\"white\">"
  43 ;;
  44
  45 let htmlfooter =
  46  " </body>" ^
  47  "</html>"
  48 ;;
  49
  50 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
  51
  52 let htmlheader_and_content = ref htmlheader;;
  53
  54 let current_cic_infos = ref None;;
  55 let current_goal_infos = ref None;;
  56 let current_scratch_infos = ref None;;
  57
  58
  59 (* MISC FUNCTIONS *)
  60
  61 let domImpl = Gdome.domImplementation ();;
  62
  63 let parseStyle name =
  64  let style =
  65   domImpl#createDocumentFromURI
  66 (*
  67    ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None
  68 *)
  69    ~uri:("styles/" ^ name) ()
  70  in
  71   Gdome_xslt.processStylesheet style
  72 ;;
  73
  74 let d_c = parseStyle "drop_coercions.xsl";;
  75 let tc1 = parseStyle "objtheorycontent.xsl";;
  76 let hc2 = parseStyle "content_to_html.xsl";;
  77 let l   = parseStyle "link.xsl";;
  78
  79 let c1 = parseStyle "rootcontent.xsl";;
  80 let g  = parseStyle "genmmlid.xsl";;
  81 let c2 = parseStyle "annotatedpres.xsl";;
  82
  83
  84 let getterURL = Configuration.getter_url;;
  85 let processorURL = Configuration.processor_url;;
  86
  87 let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
  88 let mml_args =
  89  ["processorURL", "'" ^ processorURL ^ "'" ;
  90   "getterURL", "'" ^ getterURL ^ "'" ;
  91   "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
  92   "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
  93   "UNICODEvsSYMBOL", "'symbol'" ;
  94   "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
  95   "encoding", "'iso-8859-1'" ;
  96   "media-type", "'text/html'" ;
  97   "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
  98   "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
  99   "naturalLanguage", "'yes'" ;
 100   "annotations", "'no'" ;
 101   "explodeall", "'true()'" ;
 102   "topurl", "'http://phd.cs.unibo.it/helm'" ;
 103   "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
 104 ;;
 105
 106 let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
 107 let sequent_args =
 108  ["processorURL", "'" ^ processorURL ^ "'" ;
 109   "getterURL", "'" ^ getterURL ^ "'" ;
 110   "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
 111   "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
 112   "UNICODEvsSYMBOL", "'symbol'" ;
 113   "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
 114   "encoding", "'iso-8859-1'" ;
 115   "media-type", "'text/html'" ;
 116   "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
 117   "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
 118   "naturalLanguage", "'no'" ;
 119   "annotations", "'no'" ;
 120   "explodeall", "'true()'" ;
 121   "topurl", "'http://phd.cs.unibo.it/helm'" ;
 122   "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
 123 ;;
 124
 125 let parse_file filename =
 126  let inch = open_in filename in
 127   let rec read_lines () =
 128    try
 129     let line = input_line inch in
 130      line ^ read_lines ()
 131    with
 132     End_of_file -> ""
 133   in
 134    read_lines ()
 135 ;;
 136
 137 let applyStylesheets input styles args =
 138  List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
 139   input styles
 140 ;;
 141
 142 let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types =
 143  let xml =
 144   Cic2Xml.print_object uri ids_to_inner_sorts annobj
 145  in
 146  let xmlinnertypes =
 147   Cic2Xml.print_inner_types uri ids_to_inner_sorts
 148    ids_to_inner_types
 149  in
 150   let input = Xml2Gdome.document_of_xml domImpl xml in
 151 (*CSC: We save the innertypes to disk so that we can retrieve them in the  *)
 152 (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
 153 (*CSC: local.                                                              *)
 154    Xml.pp xmlinnertypes (Some "/public/fguidi/innertypes") ;
 155    let output = applyStylesheets input mml_styles mml_args in
 156     output
 157 ;;
 158
 159
 160 (* CALLBACKS *)
 161
 162 exception RefreshSequentException of exn;;
 163 exception RefreshProofException of exn;;
 164
 165 let refresh_proof (output : GMathView.math_view) =
 166  try
 167   let uri,currentproof =
 168    match !ProofEngine.proof with
 169       None -> assert false
 170     | Some (uri,metasenv,bo,ty) ->
 171        uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty))
 172   in
 173    let
 174     (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types)
 175    =
 176     Cic2acic.acic_object_of_cic_object currentproof
 177    in
 178     let mml =
 179      mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
 180     in
 181      output#load_tree mml ;
 182      current_cic_infos := Some (ids_to_terms,ids_to_father_ids)
 183  with
 184   e -> raise (RefreshProofException e)
 185 ;;
 186
 187 let refresh_sequent (proofw : GMathView.math_view) =
 188  try
 189   match !ProofEngine.goal with
 190      None -> proofw#unload
 191    | Some (_,currentsequent) ->
 192       let metasenv =
 193        match !ProofEngine.proof with
 194           None -> assert false
 195         | Some (_,metasenv,_,_) -> metasenv
 196       in
 197        let sequent_gdome,ids_to_terms,ids_to_father_ids =
 198         SequentPp.XmlPp.print_sequent metasenv currentsequent
 199        in
 200         let sequent_doc =
 201          Xml2Gdome.document_of_xml domImpl sequent_gdome
 202         in
 203          let sequent_mml =
 204           applyStylesheets sequent_doc sequent_styles sequent_args
 205          in
 206           proofw#load_tree ~dom:sequent_mml ;
 207           current_goal_infos := Some (ids_to_terms,ids_to_father_ids)
 208  with
 209   e -> raise (RefreshSequentException e)
 210 ;;
 211
 212 (*
 213 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
 214  ~name:"/public/sacerdot/guruguru1" ~indent:true ()) ;
 215 *)
 216
 217 let mml_of_cic_term term =
 218  let context =
 219   match !ProofEngine.goal with
 220      None -> []
 221    | Some (_,(context,_)) -> context
 222  in
 223   let metasenv =
 224    match !ProofEngine.proof with
 225       None -> []
 226     | Some (_,metasenv,_,_) -> metasenv
 227   in
 228    let sequent_gdome,ids_to_terms,ids_to_father_ids =
 229     SequentPp.XmlPp.print_sequent metasenv (context,term)
 230    in
 231     let sequent_doc =
 232      Xml2Gdome.document_of_xml domImpl sequent_gdome
 233     in
 234      let res =
 235       applyStylesheets sequent_doc sequent_styles sequent_args ;
 236      in
 237       current_scratch_infos := Some (term,ids_to_terms,ids_to_father_ids) ;
 238       res
 239 ;;
 240
 241 let output_html outputhtml msg =
 242  htmlheader_and_content := !htmlheader_and_content ^ msg ;
 243  outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
 244  outputhtml#set_topline (-1)
 245 ;;
 246
 247 (***********************)
 248 (*       TACTICS       *)
 249 (***********************)
 250
 251 let call_tactic tactic rendering_window () =
 252  let proofw = (rendering_window#proofw : GMathView.math_view) in
 253  let output = (rendering_window#output : GMathView.math_view) in
 254  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 255  let savedproof = !ProofEngine.proof in
 256  let savedgoal  = !ProofEngine.goal in
 257   begin
 258    try
 259     tactic () ;
 260     refresh_sequent proofw ;
 261     refresh_proof output
 262    with
 263       RefreshSequentException e ->
 264        output_html outputhtml
 265         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 266          "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 267        ProofEngine.proof := savedproof ;
 268        ProofEngine.goal := savedgoal ;
 269        refresh_sequent proofw
 270     | RefreshProofException e ->
 271        output_html outputhtml
 272         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 273          "proof: " ^ Printexc.to_string e ^ "</h1>") ;
 274        ProofEngine.proof := savedproof ;
 275        ProofEngine.goal := savedgoal ;
 276        refresh_sequent proofw ;
 277        refresh_proof output
 278     | e ->
 279        output_html outputhtml
 280         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 281        ProofEngine.proof := savedproof ;
 282        ProofEngine.goal := savedgoal ;
 283   end
 284 ;;
 285
 286 let call_tactic_with_input tactic rendering_window () =
 287  let proofw = (rendering_window#proofw : GMathView.math_view) in
 288  let output = (rendering_window#output : GMathView.math_view) in
 289  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 290  let inputt = (rendering_window#inputt : GEdit.text) in
 291  let savedproof = !ProofEngine.proof in
 292  let savedgoal  = !ProofEngine.goal in
 293 (*CSC: Gran cut&paste da sotto... *)
 294   let inputlen = inputt#length in
 295   let input = inputt#get_chars 0 inputlen ^ "\n" in
 296    let lexbuf = Lexing.from_string input in
 297    let curi =
 298     match !ProofEngine.proof with
 299        None -> assert false
 300      | Some (curi,_,_,_) -> curi
 301    in
 302    let context =
 303     List.map
 304      (function
 305          ProofEngine.Definition (n,_)
 306        | ProofEngine.Declaration (n,_) -> n)
 307      (match !ProofEngine.goal with
 308          None -> assert false
 309        | Some (_,(ctx,_)) -> ctx
 310      )
 311    in
 312     try
 313      while true do
 314       match
 315        CicTextualParserContext.main curi context CicTextualLexer.token lexbuf
 316       with
 317          None -> ()
 318        | Some expr ->
 319           tactic expr ;
 320           refresh_sequent proofw ;
 321           refresh_proof output
 322      done
 323     with
 324        CicTextualParser0.Eof ->
 325         inputt#delete_text 0 inputlen
 326      | RefreshSequentException e ->
 327         output_html outputhtml
 328          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 329           "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 330         ProofEngine.proof := savedproof ;
 331         ProofEngine.goal := savedgoal ;
 332         refresh_sequent proofw
 333      | RefreshProofException e ->
 334         output_html outputhtml
 335          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 336           "proof: " ^ Printexc.to_string e ^ "</h1>") ;
 337         ProofEngine.proof := savedproof ;
 338         ProofEngine.goal := savedgoal ;
 339         refresh_sequent proofw ;
 340         refresh_proof output
 341      | e ->
 342         output_html outputhtml
 343          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 344         ProofEngine.proof := savedproof ;
 345         ProofEngine.goal := savedgoal ;
 346 ;;
 347
 348 let call_tactic_with_goal_input tactic rendering_window () =
 349  let module L = LogicalOperations in
 350  let module G = Gdome in
 351   let proofw = (rendering_window#proofw : GMathView.math_view) in
 352   let output = (rendering_window#output : GMathView.math_view) in
 353   let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 354   let savedproof = !ProofEngine.proof in
 355   let savedgoal  = !ProofEngine.goal in
 356    match proofw#get_selection with
 357      Some node ->
 358       let xpath =
 359        ((node : Gdome.element)#getAttributeNS
 360          ~namespaceURI:helmns
 361          ~localName:(G.domString "xref"))#to_string
 362       in
 363        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 364        else
 365         begin
 366          try
 367           match !current_goal_infos with
 368              Some (ids_to_terms, ids_to_father_ids) ->
 369               let id = xpath in
 370                tactic (Hashtbl.find ids_to_terms id) ;
 371                refresh_sequent rendering_window#proofw ;
 372                refresh_proof rendering_window#output
 373            | None -> assert false (* "ERROR: No current term!!!" *)
 374          with
 375             RefreshSequentException e ->
 376              output_html outputhtml
 377               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 378                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 379              ProofEngine.proof := savedproof ;
 380              ProofEngine.goal := savedgoal ;
 381              refresh_sequent proofw
 382           | RefreshProofException e ->
 383              output_html outputhtml
 384               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 385                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
 386              ProofEngine.proof := savedproof ;
 387              ProofEngine.goal := savedgoal ;
 388              refresh_sequent proofw ;
 389              refresh_proof output
 390           | e ->
 391              output_html outputhtml
 392               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 393              ProofEngine.proof := savedproof ;
 394              ProofEngine.goal := savedgoal ;
 395         end
 396    | None ->
 397       output_html outputhtml
 398        ("<h1 color=\"red\">No term selected</h1>")
 399 ;;
 400
 401 let call_tactic_with_input_and_goal_input tactic rendering_window () =
 402  let module L = LogicalOperations in
 403  let module G = Gdome in
 404   let proofw = (rendering_window#proofw : GMathView.math_view) in
 405   let output = (rendering_window#output : GMathView.math_view) in
 406   let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 407   let inputt = (rendering_window#inputt : GEdit.text) in
 408   let savedproof = !ProofEngine.proof in
 409   let savedgoal  = !ProofEngine.goal in
 410    match proofw#get_selection with
 411      Some node ->
 412       let xpath =
 413        ((node : Gdome.element)#getAttributeNS
 414          ~namespaceURI:helmns
 415          ~localName:(G.domString "xref"))#to_string
 416       in
 417        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 418        else
 419         begin
 420          try
 421           match !current_goal_infos with
 422              Some (ids_to_terms, ids_to_father_ids) ->
 423               let id = xpath in
 424                (* Let's parse the input *)
 425                let inputlen = inputt#length in
 426                let input = inputt#get_chars 0 inputlen ^ "\n" in
 427                 let lexbuf = Lexing.from_string input in
 428                 let curi =
 429                  match !ProofEngine.proof with
 430                     None -> assert false
 431                   | Some (curi,_,_,_) -> curi
 432                 in
 433                 let context =
 434                  List.map
 435                   (function
 436                       ProofEngine.Definition (n,_)
 437                     | ProofEngine.Declaration (n,_) -> n)
 438                   (match !ProofEngine.goal with
 439                       None -> assert false
 440                     | Some (_,(ctx,_)) -> ctx
 441                   )
 442                 in
 443                  begin
 444                   try
 445                    while true do
 446                     match
 447                      CicTextualParserContext.main curi context
 448                       CicTextualLexer.token lexbuf
 449                     with
 450                        None -> ()
 451                      | Some expr ->
 452                         tactic ~goal_input:(Hashtbl.find ids_to_terms id)
 453                          ~input:expr ;
 454                         refresh_sequent proofw ;
 455                         refresh_proof output
 456                    done
 457                   with
 458                      CicTextualParser0.Eof ->
 459                       inputt#delete_text 0 inputlen
 460                  end
 461            | None -> assert false (* "ERROR: No current term!!!" *)
 462          with
 463             RefreshSequentException e ->
 464              output_html outputhtml
 465               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 466                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 467              ProofEngine.proof := savedproof ;
 468              ProofEngine.goal := savedgoal ;
 469              refresh_sequent proofw
 470           | RefreshProofException e ->
 471              output_html outputhtml
 472               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 473                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
 474              ProofEngine.proof := savedproof ;
 475              ProofEngine.goal := savedgoal ;
 476              refresh_sequent proofw ;
 477              refresh_proof output
 478           | e ->
 479              output_html outputhtml
 480               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 481              ProofEngine.proof := savedproof ;
 482              ProofEngine.goal := savedgoal ;
 483         end
 484    | None ->
 485       output_html outputhtml
 486        ("<h1 color=\"red\">No term selected</h1>")
 487 ;;
 488
 489 let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
 490  let module L = LogicalOperations in
 491  let module G = Gdome in
 492   let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in
 493   let outputhtml = (scratch_window#outputhtml : GHtml.xmhtml) in
 494   let savedproof = !ProofEngine.proof in
 495   let savedgoal  = !ProofEngine.goal in
 496    match mmlwidget#get_selection with
 497      Some node ->
 498       let xpath =
 499        ((node : Gdome.element)#getAttributeNS
 500          ~namespaceURI:helmns
 501          ~localName:(G.domString "xref"))#to_string
 502       in
 503        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 504        else
 505         begin
 506          try
 507           match !current_scratch_infos with
 508              (* term is the whole goal in the scratch_area *)
 509              Some (term,ids_to_terms, ids_to_father_ids) ->
 510               let id = xpath in
 511                let expr = tactic term (Hashtbl.find ids_to_terms id) in
 512                 let mml = mml_of_cic_term expr in
 513                  scratch_window#show () ;
 514                  scratch_window#mmlwidget#load_tree ~dom:mml
 515            | None -> assert false (* "ERROR: No current term!!!" *)
 516          with
 517           e ->
 518            output_html outputhtml
 519             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 520         end
 521    | None ->
 522       output_html outputhtml
 523        ("<h1 color=\"red\">No term selected</h1>")
 524 ;;
 525
 526 let intros rendering_window = call_tactic ProofEngine.intros rendering_window;;
 527 let exact rendering_window =
 528  call_tactic_with_input ProofEngine.exact rendering_window
 529 ;;
 530 let apply rendering_window =
 531  call_tactic_with_input ProofEngine.apply rendering_window
 532 ;;
 533 let elimintros rendering_window =
 534  call_tactic_with_input ProofEngine.elim_intros rendering_window
 535 ;;
 536 let whd rendering_window =
 537  call_tactic_with_goal_input ProofEngine.whd rendering_window
 538 ;;
 539 let reduce rendering_window =
 540  call_tactic_with_goal_input ProofEngine.reduce rendering_window
 541 ;;
 542 let simpl rendering_window =
 543  call_tactic_with_goal_input ProofEngine.simpl rendering_window
 544 ;;
 545 let fold rendering_window =
 546  call_tactic_with_input ProofEngine.fold rendering_window
 547 ;;
 548 let cut rendering_window =
 549  call_tactic_with_input ProofEngine.cut rendering_window
 550 ;;
 551 let change rendering_window =
 552  call_tactic_with_input_and_goal_input ProofEngine.change rendering_window
 553 ;;
 554 let letin rendering_window =
 555  call_tactic_with_input ProofEngine.letin rendering_window
 556 ;;
 557
 558
 559 let whd_in_scratch scratch_window =
 560  call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
 561   scratch_window
 562 ;;
 563 let reduce_in_scratch scratch_window =
 564  call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch
 565   scratch_window
 566 ;;
 567 let simpl_in_scratch scratch_window =
 568  call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch
 569   scratch_window
 570 ;;
 571
 572
 573
 574 (**********************)
 575 (*   END OF TACTICS   *)
 576 (**********************)
 577
 578 exception OpenConjecturesStillThere;;
 579 exception WrongProof;;
 580
 581 let save rendering_window () =
 582  match !ProofEngine.proof with
 583     None -> assert false
 584   | Some (uri,[],bo,ty) ->
 585      if CicReduction.are_convertible (CicTypeChecker.type_of_aux' [] [] bo) ty then
 586       begin
 587        (*CSC: Wrong: [] is just plainly wrong *)
 588        let proof = Cic.Definition (UriManager.name_of_uri uri,bo,ty,[]) in
 589         let
 590          (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
 591           ids_to_inner_types)
 592         =
 593          Cic2acic.acic_object_of_cic_object proof
 594         in
 595          let mml =
 596           mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
 597          in
 598           (rendering_window#output : GMathView.math_view)#load_tree mml ;
 599           current_cic_infos := Some (ids_to_terms,ids_to_father_ids)
 600       end
 601      else
 602       raise WrongProof
 603   | _ -> raise OpenConjecturesStillThere
 604 ;;
 605
 606 let proveit rendering_window () =
 607  let module L = LogicalOperations in
 608  let module G = Gdome in
 609  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 610   match rendering_window#output#get_selection with
 611     Some node ->
 612      let xpath =
 613       ((node : Gdome.element)#getAttributeNS
 614       (*CSC: OCAML DIVERGE
 615       ((element : G.element)#getAttributeNS
 616       *)
 617         ~namespaceURI:helmns
 618         ~localName:(G.domString "xref"))#to_string
 619      in
 620       if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 621       else
 622        begin
 623         try
 624          match !current_cic_infos with
 625             Some (ids_to_terms, ids_to_father_ids) ->
 626              let id = xpath in
 627               if L.to_sequent id ids_to_terms ids_to_father_ids then
 628                refresh_proof rendering_window#output ;
 629               refresh_sequent rendering_window#proofw
 630           | None -> assert false (* "ERROR: No current term!!!" *)
 631         with
 632            RefreshSequentException e ->
 633             output_html outputhtml
 634              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 635               "sequent: " ^ Printexc.to_string e ^ "</h1>")
 636          | RefreshProofException e ->
 637             output_html outputhtml
 638              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 639               "proof: " ^ Printexc.to_string e ^ "</h1>")
 640          | e ->
 641             output_html outputhtml
 642              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 643        end
 644   | None -> assert false (* "ERROR: No selection!!!" *)
 645 ;;
 646
 647 exception NotADefinition;;
 648
 649 let open_ rendering_window () =
 650  let inputt = (rendering_window#inputt : GEdit.text) in
 651  let oldinputt = (rendering_window#oldinputt : GEdit.text) in
 652  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 653  let output = (rendering_window#output : GMathView.math_view) in
 654  let proofw = (rendering_window#proofw : GMathView.math_view) in
 655   let inputlen = inputt#length in
 656   let input = inputt#get_chars 0 inputlen ^ "\n" in
 657    try
 658     let uri = UriManager.uri_of_string ("cic:" ^ input) in
 659      CicTypeChecker.typecheck uri ;
 660      let metasenv,bo,ty =
 661       match CicEnvironment.get_cooked_obj uri 0 with
 662          Cic.Definition (_,bo,ty,_) -> [],bo,ty
 663        | Cic.CurrentProof (_,metasenv,bo,ty) -> metasenv,bo,ty
 664        | Cic.Axiom _
 665        | Cic.Variable _
 666        | Cic.InductiveDefinition _ -> raise NotADefinition
 667      in
 668       ProofEngine.proof :=
 669        Some (uri, metasenv, bo, ty) ;
 670       ProofEngine.goal := None ;
 671       refresh_sequent proofw ;
 672       refresh_proof output ;
 673       inputt#delete_text 0 inputlen ;
 674       ignore(oldinputt#insert_text input oldinputt#length)
 675    with
 676       RefreshSequentException e ->
 677        output_html outputhtml
 678         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 679          "sequent: " ^ Printexc.to_string e ^ "</h1>")
 680     | RefreshProofException e ->
 681        output_html outputhtml
 682         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 683          "proof: " ^ Printexc.to_string e ^ "</h1>")
 684     | e ->
 685        output_html outputhtml
 686         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 687 ;;
 688
 689 let state rendering_window () =
 690  let inputt = (rendering_window#inputt : GEdit.text) in
 691  let oldinputt = (rendering_window#oldinputt : GEdit.text) in
 692  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 693  let output = (rendering_window#output : GMathView.math_view) in
 694  let proofw = (rendering_window#proofw : GMathView.math_view) in
 695   let inputlen = inputt#length in
 696   let input = inputt#get_chars 0 inputlen ^ "\n" in
 697    (* Do something interesting *)
 698    let lexbuf = Lexing.from_string input in
 699     try
 700      while true do
 701       (* Execute the actions *)
 702       match CicTextualParser.main CicTextualLexer.token lexbuf with
 703          None -> ()
 704        | Some expr ->
 705           let _  = CicTypeChecker.type_of_aux' [] [] expr in
 706            ProofEngine.proof :=
 707             Some (UriManager.uri_of_string "cic:/dummy.con",
 708                    [1,expr], Cic.Meta 1, expr) ;
 709            ProofEngine.goal := Some (1,([],expr)) ;
 710            refresh_sequent proofw ;
 711            refresh_proof output ;
 712      done
 713     with
 714        CicTextualParser0.Eof ->
 715         inputt#delete_text 0 inputlen ;
 716         ignore(oldinputt#insert_text input oldinputt#length)
 717      | RefreshSequentException e ->
 718         output_html outputhtml
 719          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 720           "sequent: " ^ Printexc.to_string e ^ "</h1>")
 721      | RefreshProofException e ->
 722         output_html outputhtml
 723          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 724           "proof: " ^ Printexc.to_string e ^ "</h1>")
 725      | e ->
 726         output_html outputhtml
 727          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 728 ;;
 729
 730 let check rendering_window scratch_window () =
 731  let inputt = (rendering_window#inputt : GEdit.text) in
 732  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 733  let output = (rendering_window#output : GMathView.math_view) in
 734  let proofw = (rendering_window#proofw : GMathView.math_view) in
 735   let inputlen = inputt#length in
 736   let input = inputt#get_chars 0 inputlen ^ "\n" in
 737   let curi,metasenv =
 738    match !ProofEngine.proof with
 739       None -> UriManager.uri_of_string "cic:/dummy.con", []
 740     | Some (curi,metasenv,_,_) -> curi,metasenv
 741   in
 742   let ciccontext,names_context =
 743    let context =
 744     match !ProofEngine.goal with
 745        None -> []
 746      | Some (_,(ctx,_)) -> ctx
 747    in
 748     ProofEngine.cic_context_of_named_context context,
 749      List.map
 750       (function
 751           ProofEngine.Declaration (n,_)
 752         | ProofEngine.Definition (n,_) -> n
 753       ) context
 754   in
 755    (* Do something interesting *)
 756    let lexbuf = Lexing.from_string input in
 757     try
 758      while true do
 759       (* Execute the actions *)
 760       match
 761        CicTextualParserContext.main curi names_context CicTextualLexer.token
 762         lexbuf
 763       with
 764          None -> ()
 765        | Some expr ->
 766           try
 767            let ty  = CicTypeChecker.type_of_aux' metasenv ciccontext expr in
 768             let mml = mml_of_cic_term (Cic.Cast (expr,ty)) in
 769              scratch_window#show () ;
 770              scratch_window#mmlwidget#load_tree ~dom:mml
 771           with
 772            e ->
 773             print_endline ("? " ^ CicPp.ppterm expr) ;
 774             raise e
 775      done
 776     with
 777        CicTextualParser0.Eof -> ()
 778      | e ->
 779        output_html outputhtml
 780         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 781 ;;
 782
 783 let locate rendering_window () =
 784  let inputt = (rendering_window#inputt : GEdit.text) in
 785  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 786   let inputlen = inputt#length in
 787   let input = inputt#get_chars 0 inputlen in
 788    try
 789     output_html outputhtml (Mquery.locate input) ;
 790     inputt#delete_text 0 inputlen
 791    with
 792     e ->
 793      output_html outputhtml
 794       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 795 ;;
 796
 797 let backward rendering_window () =
 798    let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 799    let result =
 800       match !ProofEngine.goal with
 801          | None -> ""
 802          | Some (_, (_, t)) -> (Mquery.backward t)
 803       in
 804    output_html outputhtml result
 805
 806 let choose_selection
 807      (mmlwidget : GMathView.math_view) (element : Gdome.element option)
 808 =
 809  let module G = Gdome in
 810   let rec aux element =
 811    if element#hasAttributeNS
 812        ~namespaceURI:helmns
 813        ~localName:(G.domString "xref")
 814    then
 815      mmlwidget#set_selection (Some element)
 816    else
 817       match element#get_parentNode with
 818          None -> assert false
 819        (*CSC: OCAML DIVERGES!
 820        | Some p -> aux (new G.element_of_node p)
 821        *)
 822        | Some p -> aux (new Gdome.element_of_node p)
 823   in
 824    match element with
 825      Some x -> aux x
 826    | None   -> mmlwidget#set_selection None
 827 ;;
 828
 829 (* STUFF TO BUILD THE GTK INTERFACE *)
 830
 831 (* Stuff for the widget settings *)
 832
 833 let export_to_postscript (output : GMathView.math_view) () =
 834  output#export_to_postscript ~filename:"output.ps" ();
 835 ;;
 836
 837 let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
 838  button_set_kerning button_set_transparency button_export_to_postscript
 839  button_t1 ()
 840 =
 841  let is_set = button_t1#active in
 842   output#set_font_manager_type
 843    (if is_set then `font_manager_t1 else `font_manager_gtk) ;
 844   if is_set then
 845    begin
 846     button_set_anti_aliasing#misc#set_sensitive true ;
 847     button_set_kerning#misc#set_sensitive true ;
 848     button_set_transparency#misc#set_sensitive true ;
 849     button_export_to_postscript#misc#set_sensitive true ;
 850    end
 851   else
 852    begin
 853     button_set_anti_aliasing#misc#set_sensitive false ;
 854     button_set_kerning#misc#set_sensitive false ;
 855     button_set_transparency#misc#set_sensitive false ;
 856     button_export_to_postscript#misc#set_sensitive false ;
 857    end
 858 ;;
 859
 860 let set_anti_aliasing output button_set_anti_aliasing () =
 861  output#set_anti_aliasing button_set_anti_aliasing#active
 862 ;;
 863
 864 let set_kerning output button_set_kerning () =
 865  output#set_kerning button_set_kerning#active
 866 ;;
 867
 868 let set_transparency output button_set_transparency () =
 869  output#set_transparency button_set_transparency#active
 870 ;;
 871
 872 let changefont output font_size_spinb () =
 873  output#set_font_size font_size_spinb#value_as_int
 874 ;;
 875
 876 let set_log_verbosity output log_verbosity_spinb () =
 877  output#set_log_verbosity log_verbosity_spinb#value_as_int
 878 ;;
 879
 880 class settings_window (output : GMathView.math_view) sw
 881  button_export_to_postscript selection_changed_callback
 882 =
 883  let settings_window = GWindow.window ~title:"GtkMathView settings" () in
 884  let vbox =
 885   GPack.vbox ~packing:settings_window#add () in
 886  let table =
 887   GPack.table
 888    ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
 889    ~border_width:5 ~packing:vbox#add () in
 890  let button_t1 =
 891   GButton.toggle_button ~label:"activate t1 fonts"
 892    ~packing:(table#attach ~left:0 ~top:0) () in
 893  let button_set_anti_aliasing =
 894   GButton.toggle_button ~label:"set_anti_aliasing"
 895    ~packing:(table#attach ~left:0 ~top:1) () in
 896  let button_set_kerning =
 897   GButton.toggle_button ~label:"set_kerning"
 898    ~packing:(table#attach ~left:1 ~top:1) () in
 899  let button_set_transparency =
 900   GButton.toggle_button ~label:"set_transparency"
 901    ~packing:(table#attach ~left:2 ~top:1) () in
 902  let table =
 903   GPack.table
 904    ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
 905    ~border_width:5 ~packing:vbox#add () in
 906  let font_size_label =
 907   GMisc.label ~text:"font size:"
 908    ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
 909  let font_size_spinb =
 910   let sadj =
 911    GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
 912   in
 913    GEdit.spin_button
 914     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
 915  let log_verbosity_label =
 916   GMisc.label ~text:"log verbosity:"
 917    ~packing:(table#attach ~left:0 ~top:1) () in
 918  let log_verbosity_spinb =
 919   let sadj =
 920    GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
 921   in
 922    GEdit.spin_button
 923     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
 924  let hbox =
 925   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 926  let closeb =
 927   GButton.button ~label:"Close"
 928    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 929 object(self)
 930  method show = settings_window#show
 931  initializer
 932   button_set_anti_aliasing#misc#set_sensitive false ;
 933   button_set_kerning#misc#set_sensitive false ;
 934   button_set_transparency#misc#set_sensitive false ;
 935   (* Signals connection *)
 936   ignore(button_t1#connect#clicked
 937    (activate_t1 output button_set_anti_aliasing button_set_kerning
 938     button_set_transparency button_export_to_postscript button_t1)) ;
 939   ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
 940   ignore(button_set_anti_aliasing#connect#toggled
 941    (set_anti_aliasing output button_set_anti_aliasing));
 942   ignore(button_set_kerning#connect#toggled
 943    (set_kerning output button_set_kerning)) ;
 944   ignore(button_set_transparency#connect#toggled
 945    (set_transparency output button_set_transparency)) ;
 946   ignore(log_verbosity_spinb#connect#changed
 947    (set_log_verbosity output log_verbosity_spinb)) ;
 948   ignore(closeb#connect#clicked settings_window#misc#hide)
 949 end;;
 950
 951 (* Scratch window *)
 952
 953 class scratch_window outputhtml =
 954  let window =
 955   GWindow.window ~title:"MathML viewer" ~border_width:2 () in
 956  let vbox =
 957   GPack.vbox ~packing:window#add () in
 958  let hbox =
 959   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 960  let whdb =
 961   GButton.button ~label:"Whd"
 962    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 963  let reduceb =
 964   GButton.button ~label:"Reduce"
 965    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 966  let simplb =
 967   GButton.button ~label:"Simpl"
 968    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 969  let scrolled_window =
 970   GBin.scrolled_window ~border_width:10
 971    ~packing:(vbox#pack ~expand:true ~padding:5) () in
 972  let mmlwidget =
 973   GMathView.math_view
 974    ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
 975 object(self)
 976  method outputhtml = outputhtml
 977  method mmlwidget = mmlwidget
 978  method show () = window#misc#hide () ; window#show ()
 979  initializer
 980   ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
 981   ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
 982   ignore(whdb#connect#clicked (whd_in_scratch self)) ;
 983   ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
 984   ignore(simplb#connect#clicked (simpl_in_scratch self))
 985 end;;
 986
 987 (* Main window *)
 988
 989 class rendering_window output proofw (label : GMisc.label) =
 990  let window =
 991   GWindow.window ~title:"MathML viewer" ~border_width:2 () in
 992  let hbox0 =
 993   GPack.hbox ~packing:window#add () in
 994  let vbox =
 995   GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
 996  let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
 997  let scrolled_window0 =
 998   GBin.scrolled_window ~border_width:10
 999    ~packing:(vbox#pack ~expand:true ~padding:5) () in
1000  let _ = scrolled_window0#add output#coerce in
1001  let hbox1 =
1002   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1003  let settingsb =
1004   GButton.button ~label:"Settings"
1005    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1006  let button_export_to_postscript =
1007   GButton.button ~label:"export_to_postscript"
1008   ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1009  let saveb =
1010   GButton.button ~label:"Save"
1011    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1012  let closeb =
1013   GButton.button ~label:"Close"
1014    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1015  let hbox2 =
1016   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1017  let proveitb =
1018   GButton.button ~label:"Prove It"
1019    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1020  let oldinputt = GEdit.text ~editable:false ~width:400 ~height:180
1021    ~packing:(vbox#pack ~padding:5) () in
1022  let hbox4 =
1023   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1024  let stateb =
1025   GButton.button ~label:"State"
1026    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1027  let openb =
1028   GButton.button ~label:"Open"
1029    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1030  let checkb =
1031   GButton.button ~label:"Check"
1032    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1033  let locateb =
1034   GButton.button ~label:"Locate"
1035    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1036  let backwardb =
1037   GButton.button ~label:"Backward"
1038    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1039  let inputt = GEdit.text ~editable:true ~width:400 ~height: 100
1040    ~packing:(vbox#pack ~padding:5) () in
1041  let vbox1 =
1042   GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1043  let scrolled_window1 =
1044   GBin.scrolled_window ~border_width:10
1045    ~packing:(vbox1#pack ~expand:true ~padding:5) () in
1046  let _ = scrolled_window1#add proofw#coerce in
1047  let hbox3 =
1048   GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1049  let exactb =
1050   GButton.button ~label:"Exact"
1051    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1052  let introsb =
1053   GButton.button ~label:"Intros"
1054    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1055  let applyb =
1056   GButton.button ~label:"Apply"
1057    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1058  let elimintrosb =
1059   GButton.button ~label:"ElimIntros"
1060    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1061  let whdb =
1062   GButton.button ~label:"Whd"
1063    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1064  let reduceb =
1065   GButton.button ~label:"Reduce"
1066    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1067  let simplb =
1068   GButton.button ~label:"Simpl"
1069    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1070  let foldb =
1071   GButton.button ~label:"Fold"
1072    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1073  let cutb =
1074   GButton.button ~label:"Cut"
1075    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1076  let changeb =
1077   GButton.button ~label:"Change"
1078    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1079  let letinb =
1080   GButton.button ~label:"Let ... In"
1081    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1082  let outputhtml =
1083   GHtml.xmhtml
1084    ~source:"<html><body bgColor=\"white\"></body></html>"
1085    ~width:400 ~height: 200
1086    ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5)
1087    ~show:true () in
1088  let scratch_window = new scratch_window outputhtml in
1089 object(self)
1090  method outputhtml = outputhtml
1091  method oldinputt = oldinputt
1092  method inputt = inputt
1093  method output = (output : GMathView.math_view)
1094  method proofw = (proofw : GMathView.math_view)
1095  method show = window#show
1096  initializer
1097   button_export_to_postscript#misc#set_sensitive false ;
1098
1099   (* signal handlers here *)
1100   ignore(output#connect#selection_changed
1101    (function elem -> proofw#unload ; choose_selection output elem)) ;
1102   ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
1103   ignore(closeb#connect#clicked (fun _ -> GMain.Main.quit ())) ;
1104   let settings_window = new settings_window output scrolled_window0
1105    button_export_to_postscript (choose_selection output) in
1106   ignore(settingsb#connect#clicked settings_window#show) ;
1107   ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
1108   ignore(saveb#connect#clicked (save self)) ;
1109   ignore(proveitb#connect#clicked (proveit self)) ;
1110   ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
1111   ignore(stateb#connect#clicked (state self)) ;
1112   ignore(openb#connect#clicked (open_ self)) ;
1113   ignore(checkb#connect#clicked (check self scratch_window)) ;
1114   ignore(locateb#connect#clicked (locate self)) ;
1115   ignore(backwardb#connect#clicked (backward self)) ;
1116   ignore(exactb#connect#clicked (exact self)) ;
1117   ignore(applyb#connect#clicked (apply self)) ;
1118   ignore(elimintrosb#connect#clicked (elimintros self)) ;
1119   ignore(whdb#connect#clicked (whd self)) ;
1120   ignore(reduceb#connect#clicked (reduce self)) ;
1121   ignore(simplb#connect#clicked (simpl self)) ;
1122   ignore(foldb#connect#clicked (fold self)) ;
1123   ignore(cutb#connect#clicked (cut self)) ;
1124   ignore(changeb#connect#clicked (change self)) ;
1125   ignore(letinb#connect#clicked (letin self)) ;
1126   ignore(introsb#connect#clicked (intros self)) ;
1127   Logger.log_callback :=
1128    (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
1129 end;;
1130
1131 (* MAIN *)
1132
1133 let initialize_everything () =
1134  let module U = Unix in
1135   let output = GMathView.math_view ~width:400 ~height:280 ()
1136   and proofw = GMathView.math_view ~width:400 ~height:275 ()
1137   and label = GMisc.label ~text:"gTopLevel" () in
1138     let rendering_window =
1139      new rendering_window output proofw label
1140     in
1141      rendering_window#show () ;
1142      GMain.Main.main ()
1143 ;;
1144
1145 let _ =
1146  CicCooking.init () ;
1147  ignore (GtkMain.Main.init ()) ;
1148  initialize_everything ()
1149 ;;