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
 586       CicReduction.are_convertible []
 587        (CicTypeChecker.type_of_aux' [] [] bo) ty
 588      then
 589       begin
 590        (*CSC: Wrong: [] is just plainly wrong *)
 591        let proof = Cic.Definition (UriManager.name_of_uri uri,bo,ty,[]) in
 592         let
 593          (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
 594           ids_to_inner_types)
 595         =
 596          Cic2acic.acic_object_of_cic_object proof
 597         in
 598          let mml =
 599           mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
 600          in
 601           (rendering_window#output : GMathView.math_view)#load_tree mml ;
 602           current_cic_infos := Some (ids_to_terms,ids_to_father_ids)
 603       end
 604      else
 605       raise WrongProof
 606   | _ -> raise OpenConjecturesStillThere
 607 ;;
 608
 609 let proveit rendering_window () =
 610  let module L = LogicalOperations in
 611  let module G = Gdome in
 612  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 613   match rendering_window#output#get_selection with
 614     Some node ->
 615      let xpath =
 616       ((node : Gdome.element)#getAttributeNS
 617       (*CSC: OCAML DIVERGE
 618       ((element : G.element)#getAttributeNS
 619       *)
 620         ~namespaceURI:helmns
 621         ~localName:(G.domString "xref"))#to_string
 622      in
 623       if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 624       else
 625        begin
 626         try
 627          match !current_cic_infos with
 628             Some (ids_to_terms, ids_to_father_ids) ->
 629              let id = xpath in
 630               if L.to_sequent id ids_to_terms ids_to_father_ids then
 631                refresh_proof rendering_window#output ;
 632               refresh_sequent rendering_window#proofw
 633           | None -> assert false (* "ERROR: No current term!!!" *)
 634         with
 635            RefreshSequentException e ->
 636             output_html outputhtml
 637              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 638               "sequent: " ^ Printexc.to_string e ^ "</h1>")
 639          | RefreshProofException e ->
 640             output_html outputhtml
 641              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 642               "proof: " ^ Printexc.to_string e ^ "</h1>")
 643          | e ->
 644             output_html outputhtml
 645              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 646        end
 647   | None -> assert false (* "ERROR: No selection!!!" *)
 648 ;;
 649
 650 exception NotADefinition;;
 651
 652 let open_ rendering_window () =
 653  let inputt = (rendering_window#inputt : GEdit.text) in
 654  let oldinputt = (rendering_window#oldinputt : GEdit.text) in
 655  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 656  let output = (rendering_window#output : GMathView.math_view) in
 657  let proofw = (rendering_window#proofw : GMathView.math_view) in
 658   let inputlen = inputt#length in
 659   let input = inputt#get_chars 0 inputlen ^ "\n" in
 660    try
 661     let uri = UriManager.uri_of_string ("cic:" ^ input) in
 662      CicTypeChecker.typecheck uri ;
 663      let metasenv,bo,ty =
 664       match CicEnvironment.get_cooked_obj uri 0 with
 665          Cic.Definition (_,bo,ty,_) -> [],bo,ty
 666        | Cic.CurrentProof (_,metasenv,bo,ty) -> metasenv,bo,ty
 667        | Cic.Axiom _
 668        | Cic.Variable _
 669        | Cic.InductiveDefinition _ -> raise NotADefinition
 670      in
 671       ProofEngine.proof :=
 672        Some (uri, metasenv, bo, ty) ;
 673       ProofEngine.goal := None ;
 674       refresh_sequent proofw ;
 675       refresh_proof output ;
 676       inputt#delete_text 0 inputlen ;
 677       ignore(oldinputt#insert_text input oldinputt#length)
 678    with
 679       RefreshSequentException e ->
 680        output_html outputhtml
 681         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 682          "sequent: " ^ Printexc.to_string e ^ "</h1>")
 683     | RefreshProofException e ->
 684        output_html outputhtml
 685         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 686          "proof: " ^ Printexc.to_string e ^ "</h1>")
 687     | e ->
 688        output_html outputhtml
 689         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 690 ;;
 691
 692 let state rendering_window () =
 693  let inputt = (rendering_window#inputt : GEdit.text) in
 694  let oldinputt = (rendering_window#oldinputt : GEdit.text) in
 695  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 696  let output = (rendering_window#output : GMathView.math_view) in
 697  let proofw = (rendering_window#proofw : GMathView.math_view) in
 698   let inputlen = inputt#length in
 699   let input = inputt#get_chars 0 inputlen ^ "\n" in
 700    (* Do something interesting *)
 701    let lexbuf = Lexing.from_string input in
 702     try
 703      while true do
 704       (* Execute the actions *)
 705       match CicTextualParser.main CicTextualLexer.token lexbuf with
 706          None -> ()
 707        | Some expr ->
 708           let _  = CicTypeChecker.type_of_aux' [] [] expr in
 709            ProofEngine.proof :=
 710             Some (UriManager.uri_of_string "cic:/dummy.con",
 711                    [1,expr], Cic.Meta 1, expr) ;
 712            ProofEngine.goal := Some (1,([],expr)) ;
 713            refresh_sequent proofw ;
 714            refresh_proof output ;
 715      done
 716     with
 717        CicTextualParser0.Eof ->
 718         inputt#delete_text 0 inputlen ;
 719         ignore(oldinputt#insert_text input oldinputt#length)
 720      | RefreshSequentException e ->
 721         output_html outputhtml
 722          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 723           "sequent: " ^ Printexc.to_string e ^ "</h1>")
 724      | RefreshProofException e ->
 725         output_html outputhtml
 726          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 727           "proof: " ^ Printexc.to_string e ^ "</h1>")
 728      | e ->
 729         output_html outputhtml
 730          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 731 ;;
 732
 733 let check rendering_window scratch_window () =
 734  let inputt = (rendering_window#inputt : GEdit.text) in
 735  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 736  let output = (rendering_window#output : GMathView.math_view) in
 737  let proofw = (rendering_window#proofw : GMathView.math_view) in
 738   let inputlen = inputt#length in
 739   let input = inputt#get_chars 0 inputlen ^ "\n" in
 740   let curi,metasenv =
 741    match !ProofEngine.proof with
 742       None -> UriManager.uri_of_string "cic:/dummy.con", []
 743     | Some (curi,metasenv,_,_) -> curi,metasenv
 744   in
 745   let ciccontext,names_context =
 746    let context =
 747     match !ProofEngine.goal with
 748        None -> []
 749      | Some (_,(ctx,_)) -> ctx
 750    in
 751     ProofEngine.cic_context_of_named_context context,
 752      List.map
 753       (function
 754           ProofEngine.Declaration (n,_)
 755         | ProofEngine.Definition (n,_) -> n
 756       ) context
 757   in
 758    (* Do something interesting *)
 759    let lexbuf = Lexing.from_string input in
 760     try
 761      while true do
 762       (* Execute the actions *)
 763       match
 764        CicTextualParserContext.main curi names_context CicTextualLexer.token
 765         lexbuf
 766       with
 767          None -> ()
 768        | Some expr ->
 769           try
 770            let ty  = CicTypeChecker.type_of_aux' metasenv ciccontext expr in
 771             let mml = mml_of_cic_term (Cic.Cast (expr,ty)) in
 772              scratch_window#show () ;
 773              scratch_window#mmlwidget#load_tree ~dom:mml
 774           with
 775            e ->
 776             print_endline ("? " ^ CicPp.ppterm expr) ;
 777             raise e
 778      done
 779     with
 780        CicTextualParser0.Eof -> ()
 781      | e ->
 782        output_html outputhtml
 783         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 784 ;;
 785
 786 let locate rendering_window () =
 787  let inputt = (rendering_window#inputt : GEdit.text) in
 788  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 789   let inputlen = inputt#length in
 790   let input = inputt#get_chars 0 inputlen in
 791    try
 792     output_html outputhtml (Mquery.locate input) ;
 793     inputt#delete_text 0 inputlen
 794    with
 795     e ->
 796      output_html outputhtml
 797       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 798 ;;
 799
 800 let backward rendering_window () =
 801    let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 802    let result =
 803       match !ProofEngine.goal with
 804          | None -> ""
 805          | Some (_, (_, t)) -> (Mquery.backward t)
 806       in
 807    output_html outputhtml result
 808
 809 let choose_selection
 810      (mmlwidget : GMathView.math_view) (element : Gdome.element option)
 811 =
 812  let module G = Gdome in
 813   let rec aux element =
 814    if element#hasAttributeNS
 815        ~namespaceURI:helmns
 816        ~localName:(G.domString "xref")
 817    then
 818      mmlwidget#set_selection (Some element)
 819    else
 820       match element#get_parentNode with
 821          None -> assert false
 822        (*CSC: OCAML DIVERGES!
 823        | Some p -> aux (new G.element_of_node p)
 824        *)
 825        | Some p -> aux (new Gdome.element_of_node p)
 826   in
 827    match element with
 828      Some x -> aux x
 829    | None   -> mmlwidget#set_selection None
 830 ;;
 831
 832 (* STUFF TO BUILD THE GTK INTERFACE *)
 833
 834 (* Stuff for the widget settings *)
 835
 836 let export_to_postscript (output : GMathView.math_view) () =
 837  output#export_to_postscript ~filename:"output.ps" ();
 838 ;;
 839
 840 let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
 841  button_set_kerning button_set_transparency button_export_to_postscript
 842  button_t1 ()
 843 =
 844  let is_set = button_t1#active in
 845   output#set_font_manager_type
 846    (if is_set then `font_manager_t1 else `font_manager_gtk) ;
 847   if is_set then
 848    begin
 849     button_set_anti_aliasing#misc#set_sensitive true ;
 850     button_set_kerning#misc#set_sensitive true ;
 851     button_set_transparency#misc#set_sensitive true ;
 852     button_export_to_postscript#misc#set_sensitive true ;
 853    end
 854   else
 855    begin
 856     button_set_anti_aliasing#misc#set_sensitive false ;
 857     button_set_kerning#misc#set_sensitive false ;
 858     button_set_transparency#misc#set_sensitive false ;
 859     button_export_to_postscript#misc#set_sensitive false ;
 860    end
 861 ;;
 862
 863 let set_anti_aliasing output button_set_anti_aliasing () =
 864  output#set_anti_aliasing button_set_anti_aliasing#active
 865 ;;
 866
 867 let set_kerning output button_set_kerning () =
 868  output#set_kerning button_set_kerning#active
 869 ;;
 870
 871 let set_transparency output button_set_transparency () =
 872  output#set_transparency button_set_transparency#active
 873 ;;
 874
 875 let changefont output font_size_spinb () =
 876  output#set_font_size font_size_spinb#value_as_int
 877 ;;
 878
 879 let set_log_verbosity output log_verbosity_spinb () =
 880  output#set_log_verbosity log_verbosity_spinb#value_as_int
 881 ;;
 882
 883 class settings_window (output : GMathView.math_view) sw
 884  button_export_to_postscript selection_changed_callback
 885 =
 886  let settings_window = GWindow.window ~title:"GtkMathView settings" () in
 887  let vbox =
 888   GPack.vbox ~packing:settings_window#add () in
 889  let table =
 890   GPack.table
 891    ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
 892    ~border_width:5 ~packing:vbox#add () in
 893  let button_t1 =
 894   GButton.toggle_button ~label:"activate t1 fonts"
 895    ~packing:(table#attach ~left:0 ~top:0) () in
 896  let button_set_anti_aliasing =
 897   GButton.toggle_button ~label:"set_anti_aliasing"
 898    ~packing:(table#attach ~left:0 ~top:1) () in
 899  let button_set_kerning =
 900   GButton.toggle_button ~label:"set_kerning"
 901    ~packing:(table#attach ~left:1 ~top:1) () in
 902  let button_set_transparency =
 903   GButton.toggle_button ~label:"set_transparency"
 904    ~packing:(table#attach ~left:2 ~top:1) () in
 905  let table =
 906   GPack.table
 907    ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
 908    ~border_width:5 ~packing:vbox#add () in
 909  let font_size_label =
 910   GMisc.label ~text:"font size:"
 911    ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
 912  let font_size_spinb =
 913   let sadj =
 914    GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
 915   in
 916    GEdit.spin_button
 917     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
 918  let log_verbosity_label =
 919   GMisc.label ~text:"log verbosity:"
 920    ~packing:(table#attach ~left:0 ~top:1) () in
 921  let log_verbosity_spinb =
 922   let sadj =
 923    GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
 924   in
 925    GEdit.spin_button
 926     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
 927  let hbox =
 928   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 929  let closeb =
 930   GButton.button ~label:"Close"
 931    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 932 object(self)
 933  method show = settings_window#show
 934  initializer
 935   button_set_anti_aliasing#misc#set_sensitive false ;
 936   button_set_kerning#misc#set_sensitive false ;
 937   button_set_transparency#misc#set_sensitive false ;
 938   (* Signals connection *)
 939   ignore(button_t1#connect#clicked
 940    (activate_t1 output button_set_anti_aliasing button_set_kerning
 941     button_set_transparency button_export_to_postscript button_t1)) ;
 942   ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
 943   ignore(button_set_anti_aliasing#connect#toggled
 944    (set_anti_aliasing output button_set_anti_aliasing));
 945   ignore(button_set_kerning#connect#toggled
 946    (set_kerning output button_set_kerning)) ;
 947   ignore(button_set_transparency#connect#toggled
 948    (set_transparency output button_set_transparency)) ;
 949   ignore(log_verbosity_spinb#connect#changed
 950    (set_log_verbosity output log_verbosity_spinb)) ;
 951   ignore(closeb#connect#clicked settings_window#misc#hide)
 952 end;;
 953
 954 (* Scratch window *)
 955
 956 class scratch_window outputhtml =
 957  let window =
 958   GWindow.window ~title:"MathML viewer" ~border_width:2 () in
 959  let vbox =
 960   GPack.vbox ~packing:window#add () in
 961  let hbox =
 962   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 963  let whdb =
 964   GButton.button ~label:"Whd"
 965    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 966  let reduceb =
 967   GButton.button ~label:"Reduce"
 968    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 969  let simplb =
 970   GButton.button ~label:"Simpl"
 971    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 972  let scrolled_window =
 973   GBin.scrolled_window ~border_width:10
 974    ~packing:(vbox#pack ~expand:true ~padding:5) () in
 975  let mmlwidget =
 976   GMathView.math_view
 977    ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
 978 object(self)
 979  method outputhtml = outputhtml
 980  method mmlwidget = mmlwidget
 981  method show () = window#misc#hide () ; window#show ()
 982  initializer
 983   ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
 984   ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
 985   ignore(whdb#connect#clicked (whd_in_scratch self)) ;
 986   ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
 987   ignore(simplb#connect#clicked (simpl_in_scratch self))
 988 end;;
 989
 990 (* Main window *)
 991
 992 class rendering_window output proofw (label : GMisc.label) =
 993  let window =
 994   GWindow.window ~title:"MathML viewer" ~border_width:2 () in
 995  let hbox0 =
 996   GPack.hbox ~packing:window#add () in
 997  let vbox =
 998   GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
 999  let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
1000  let scrolled_window0 =
1001   GBin.scrolled_window ~border_width:10
1002    ~packing:(vbox#pack ~expand:true ~padding:5) () in
1003  let _ = scrolled_window0#add output#coerce in
1004  let hbox1 =
1005   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1006  let settingsb =
1007   GButton.button ~label:"Settings"
1008    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1009  let button_export_to_postscript =
1010   GButton.button ~label:"export_to_postscript"
1011   ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1012  let saveb =
1013   GButton.button ~label:"Save"
1014    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1015  let closeb =
1016   GButton.button ~label:"Close"
1017    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1018  let hbox2 =
1019   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1020  let proveitb =
1021   GButton.button ~label:"Prove It"
1022    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1023  let oldinputt = GEdit.text ~editable:false ~width:400 ~height:180
1024    ~packing:(vbox#pack ~padding:5) () in
1025  let hbox4 =
1026   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1027  let stateb =
1028   GButton.button ~label:"State"
1029    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1030  let openb =
1031   GButton.button ~label:"Open"
1032    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1033  let checkb =
1034   GButton.button ~label:"Check"
1035    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1036  let locateb =
1037   GButton.button ~label:"Locate"
1038    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1039  let backwardb =
1040   GButton.button ~label:"Backward"
1041    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1042  let inputt = GEdit.text ~editable:true ~width:400 ~height: 100
1043    ~packing:(vbox#pack ~padding:5) () in
1044  let vbox1 =
1045   GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1046  let scrolled_window1 =
1047   GBin.scrolled_window ~border_width:10
1048    ~packing:(vbox1#pack ~expand:true ~padding:5) () in
1049  let _ = scrolled_window1#add proofw#coerce in
1050  let hbox3 =
1051   GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1052  let exactb =
1053   GButton.button ~label:"Exact"
1054    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1055  let introsb =
1056   GButton.button ~label:"Intros"
1057    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1058  let applyb =
1059   GButton.button ~label:"Apply"
1060    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1061  let elimintrosb =
1062   GButton.button ~label:"ElimIntros"
1063    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1064  let whdb =
1065   GButton.button ~label:"Whd"
1066    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1067  let reduceb =
1068   GButton.button ~label:"Reduce"
1069    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1070  let simplb =
1071   GButton.button ~label:"Simpl"
1072    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1073  let foldb =
1074   GButton.button ~label:"Fold"
1075    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1076  let cutb =
1077   GButton.button ~label:"Cut"
1078    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1079  let changeb =
1080   GButton.button ~label:"Change"
1081    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1082  let letinb =
1083   GButton.button ~label:"Let ... In"
1084    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1085  let outputhtml =
1086   GHtml.xmhtml
1087    ~source:"<html><body bgColor=\"white\"></body></html>"
1088    ~width:400 ~height: 200
1089    ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5)
1090    ~show:true () in
1091  let scratch_window = new scratch_window outputhtml in
1092 object(self)
1093  method outputhtml = outputhtml
1094  method oldinputt = oldinputt
1095  method inputt = inputt
1096  method output = (output : GMathView.math_view)
1097  method proofw = (proofw : GMathView.math_view)
1098  method show = window#show
1099  initializer
1100   button_export_to_postscript#misc#set_sensitive false ;
1101
1102   (* signal handlers here *)
1103   ignore(output#connect#selection_changed
1104    (function elem -> proofw#unload ; choose_selection output elem)) ;
1105   ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
1106   ignore(closeb#connect#clicked (fun _ -> GMain.Main.quit ())) ;
1107   let settings_window = new settings_window output scrolled_window0
1108    button_export_to_postscript (choose_selection output) in
1109   ignore(settingsb#connect#clicked settings_window#show) ;
1110   ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
1111   ignore(saveb#connect#clicked (save self)) ;
1112   ignore(proveitb#connect#clicked (proveit self)) ;
1113   ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
1114   ignore(stateb#connect#clicked (state self)) ;
1115   ignore(openb#connect#clicked (open_ self)) ;
1116   ignore(checkb#connect#clicked (check self scratch_window)) ;
1117   ignore(locateb#connect#clicked (locate self)) ;
1118   ignore(backwardb#connect#clicked (backward self)) ;
1119   ignore(exactb#connect#clicked (exact self)) ;
1120   ignore(applyb#connect#clicked (apply self)) ;
1121   ignore(elimintrosb#connect#clicked (elimintros self)) ;
1122   ignore(whdb#connect#clicked (whd self)) ;
1123   ignore(reduceb#connect#clicked (reduce self)) ;
1124   ignore(simplb#connect#clicked (simpl self)) ;
1125   ignore(foldb#connect#clicked (fold self)) ;
1126   ignore(cutb#connect#clicked (cut self)) ;
1127   ignore(changeb#connect#clicked (change self)) ;
1128   ignore(letinb#connect#clicked (letin self)) ;
1129   ignore(introsb#connect#clicked (intros self)) ;
1130   Logger.log_callback :=
1131    (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
1132 end;;
1133
1134 (* MAIN *)
1135
1136 let initialize_everything () =
1137  let module U = Unix in
1138   let output = GMathView.math_view ~width:400 ~height:280 ()
1139   and proofw = GMathView.math_view ~width:400 ~height:275 ()
1140   and label = GMisc.label ~text:"gTopLevel" () in
1141     let rendering_window =
1142      new rendering_window output proofw label
1143     in
1144      rendering_window#show () ;
1145      GMain.Main.main ()
1146 ;;
1147
1148 let _ =
1149  CicCooking.init () ;
1150  ignore (GtkMain.Main.init ()) ;
1151  initialize_everything ()
1152 ;;