helm/gTopLevel/gTopLevel.ml

   1 (* Copyright (C) 2000-2002, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (******************************************************************************)
  27 (*                                                                            *)
  28 (*                               PROJECT HELM                                 *)
  29 (*                                                                            *)
  30 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
  31 (*                                 06/01/2002                                 *)
  32 (*                                                                            *)
  33 (*                                                                            *)
  34 (******************************************************************************)
  35
  36
  37 (* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *)
  38 let wrong_xpointer_format_from_wrong_xpointer_format' uri =
  39  try
  40   let index_sharp =  String.index uri '#' in
  41   let index_rest = index_sharp + 10 in
  42    let baseuri = String.sub uri 0 index_sharp in
  43    let rest = String.sub uri index_rest (String.length uri - index_rest - 1) in
  44     baseuri ^ "#" ^ rest
  45  with Not_found -> uri
  46 ;;
  47
  48 (* GLOBAL CONSTANTS *)
  49
  50 let helmns = Gdome.domString "http://www.cs.unibo.it/helm";;
  51
  52 let htmlheader =
  53  "<html>" ^
  54  " <body bgColor=\"white\">"
  55 ;;
  56
  57 let htmlfooter =
  58  " </body>" ^
  59  "</html>"
  60 ;;
  61
  62 (*
  63 let prooffile = "/home/tassi/miohelm/tmp/currentproof";;
  64 let prooffile = "/public/sacerdot/currentproof";;
  65 *)
  66
  67 let prooffile = "/public/sacerdot/currentproof";;
  68 let prooffiletype = "/public/sacerdot/currentprooftype";;
  69
  70 (*CSC: the getter should handle the innertypes, not the FS *)
  71 (*
  72 let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";;
  73 let innertypesfile = "/public/sacerdot/innertypes";;
  74 *)
  75
  76 let innertypesfile = "/public/sacerdot/innertypes";;
  77 let constanttypefile = "/public/sacerdot/constanttype";;
  78
  79
  80 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
  81
  82 let htmlheader_and_content = ref htmlheader;;
  83
  84 let current_cic_infos = ref None;;
  85 let current_goal_infos = ref None;;
  86 let current_scratch_infos = ref None;;
  87
  88 (* COMMAND LINE OPTIONS *)
  89
  90 let usedb = ref true
  91
  92 let argspec =
  93   [
  94     "-nodb", Arg.Clear usedb, "disable use of MathQL DB"
  95   ]
  96 in
  97 Arg.parse argspec ignore ""
  98
  99
 100 (* MISC FUNCTIONS *)
 101
 102 let cic_textual_parser_uri_of_uri uri' =
 103  (* Constant *)
 104  if String.sub uri' (String.length uri' - 4) 4 = ".con" then
 105   CicTextualParser0.ConUri (UriManager.uri_of_string uri')
 106  else
 107   if String.sub uri' (String.length uri' - 4) 4 = ".var" then
 108    CicTextualParser0.VarUri (UriManager.uri_of_string uri')
 109   else
 110    (try
 111      (* Inductive Type *)
 112      let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
 113       CicTextualParser0.IndTyUri (uri'',typeno)
 114     with
 115      _ ->
 116       (* Constructor of an Inductive Type *)
 117       let uri'',typeno,consno =
 118        CicTextualLexer.indconuri_of_uri uri'
 119       in
 120        CicTextualParser0.IndConUri (uri'',typeno,consno)
 121    )
 122 ;;
 123
 124 let term_of_uri uri =
 125  let module C = Cic in
 126  let module CTP = CicTextualParser0 in
 127   match (cic_textual_parser_uri_of_uri uri) with
 128      CTP.ConUri uri -> C.Const (uri,[])
 129    | CTP.VarUri uri -> C.Var (uri,[])
 130    | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[])
 131    | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[])
 132 ;;
 133
 134 let domImpl = Gdome.domImplementation ();;
 135
 136 let parseStyle name =
 137  let style =
 138   domImpl#createDocumentFromURI
 139 (*
 140    ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None
 141 *)
 142    ~uri:("styles/" ^ name) ()
 143  in
 144   Gdome_xslt.processStylesheet style
 145 ;;
 146
 147 let d_c = parseStyle "drop_coercions.xsl";;
 148 let tc1 = parseStyle "objtheorycontent.xsl";;
 149 let hc2 = parseStyle "content_to_html.xsl";;
 150 let l   = parseStyle "link.xsl";;
 151
 152 let c1 = parseStyle "rootcontent.xsl";;
 153 let g  = parseStyle "genmmlid.xsl";;
 154 let c2 = parseStyle "annotatedpres.xsl";;
 155
 156
 157 let getterURL = Configuration.getter_url;;
 158 let processorURL = Configuration.processor_url;;
 159
 160 let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
 161 let mml_args =
 162  ["processorURL", "'" ^ processorURL ^ "'" ;
 163   "getterURL", "'" ^ getterURL ^ "'" ;
 164   "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
 165   "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
 166   "UNICODEvsSYMBOL", "'symbol'" ;
 167   "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
 168   "encoding", "'iso-8859-1'" ;
 169   "media-type", "'text/html'" ;
 170   "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
 171   "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
 172   "naturalLanguage", "'yes'" ;
 173   "annotations", "'no'" ;
 174   "explodeall", "'true()'" ;
 175   "topurl", "'http://phd.cs.unibo.it/helm'" ;
 176   "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
 177 ;;
 178
 179 let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
 180 let sequent_args =
 181  ["processorURL", "'" ^ processorURL ^ "'" ;
 182   "getterURL", "'" ^ getterURL ^ "'" ;
 183   "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
 184   "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
 185   "UNICODEvsSYMBOL", "'symbol'" ;
 186   "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
 187   "encoding", "'iso-8859-1'" ;
 188   "media-type", "'text/html'" ;
 189   "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
 190   "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
 191   "naturalLanguage", "'no'" ;
 192   "annotations", "'no'" ;
 193   "explodeall", "'true()'" ;
 194   "topurl", "'http://phd.cs.unibo.it/helm'" ;
 195   "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
 196 ;;
 197
 198 let parse_file filename =
 199  let inch = open_in filename in
 200   let rec read_lines () =
 201    try
 202     let line = input_line inch in
 203      line ^ read_lines ()
 204    with
 205     End_of_file -> ""
 206   in
 207    read_lines ()
 208 ;;
 209
 210 let applyStylesheets input styles args =
 211  List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
 212   input styles
 213 ;;
 214
 215 let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types =
 216 (*CSC: ????????????????? *)
 217  let xml, bodyxml =
 218   Cic2Xml.print_object uri ~ids_to_inner_sorts annobj
 219  in
 220  let xmlinnertypes =
 221   Cic2Xml.print_inner_types uri ~ids_to_inner_sorts
 222    ~ids_to_inner_types
 223  in
 224   let input =
 225    match bodyxml with
 226       None -> Xml2Gdome.document_of_xml domImpl xml
 227     | Some bodyxml' ->
 228        Xml.pp xml (Some constanttypefile) ;
 229        Xml2Gdome.document_of_xml domImpl bodyxml'
 230   in
 231 (*CSC: We save the innertypes to disk so that we can retrieve them in the  *)
 232 (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
 233 (*CSC: local.                                                              *)
 234    Xml.pp xmlinnertypes (Some innertypesfile) ;
 235    let output = applyStylesheets input mml_styles mml_args in
 236     output
 237 ;;
 238
 239
 240 (* CALLBACKS *)
 241
 242 exception RefreshSequentException of exn;;
 243 exception RefreshProofException of exn;;
 244
 245 let refresh_proof (output : GMathView.math_view) =
 246  try
 247   let uri,currentproof =
 248    match !ProofEngine.proof with
 249       None -> assert false
 250     | Some (uri,metasenv,bo,ty) ->
 251        (*CSC: Wrong: [] is just plainly wrong *)
 252        uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
 253   in
 254    let
 255     (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
 256      ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
 257    =
 258     Cic2acic.acic_object_of_cic_object currentproof
 259    in
 260     let mml =
 261      mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
 262     in
 263      output#load_tree mml ;
 264      current_cic_infos :=
 265       Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses)
 266  with
 267   e ->
 268  match !ProofEngine.proof with
 269     None -> assert false
 270   | Some (uri,metasenv,bo,ty) ->
 271 prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
 272    raise (RefreshProofException e)
 273 ;;
 274
 275 let refresh_sequent (proofw : GMathView.math_view) =
 276  try
 277   match !ProofEngine.goal with
 278      None -> proofw#unload
 279    | Some metano ->
 280       let metasenv =
 281        match !ProofEngine.proof with
 282           None -> assert false
 283         | Some (_,metasenv,_,_) -> metasenv
 284       in
 285       let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
 286        let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
 287         SequentPp.XmlPp.print_sequent metasenv currentsequent
 288        in
 289         let sequent_doc =
 290          Xml2Gdome.document_of_xml domImpl sequent_gdome
 291         in
 292          let sequent_mml =
 293           applyStylesheets sequent_doc sequent_styles sequent_args
 294          in
 295           proofw#load_tree ~dom:sequent_mml ;
 296           current_goal_infos :=
 297            Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
 298  with
 299   e ->
 300 let metano =
 301   match !ProofEngine.goal with
 302      None -> assert false
 303    | Some m -> m
 304 in
 305 let metasenv =
 306  match !ProofEngine.proof with
 307     None -> assert false
 308   | Some (_,metasenv,_,_) -> metasenv
 309 in
 310 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
 311 prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
 312    raise (RefreshSequentException e)
 313 ;;
 314
 315 (*
 316 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
 317  ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ;
 318 *)
 319
 320 let mml_of_cic_term metano term =
 321  let metasenv =
 322   match !ProofEngine.proof with
 323      None -> []
 324    | Some (_,metasenv,_,_) -> metasenv
 325  in
 326  let context =
 327   match !ProofEngine.goal with
 328      None -> []
 329    | Some metano ->
 330       let (_,canonical_context,_) =
 331        List.find (function (m,_,_) -> m=metano) metasenv
 332       in
 333        canonical_context
 334  in
 335    let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
 336     SequentPp.XmlPp.print_sequent metasenv (metano,context,term)
 337    in
 338     let sequent_doc =
 339      Xml2Gdome.document_of_xml domImpl sequent_gdome
 340     in
 341      let res =
 342       applyStylesheets sequent_doc sequent_styles sequent_args ;
 343      in
 344       current_scratch_infos :=
 345        Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ;
 346       res
 347 ;;
 348
 349 let output_html outputhtml msg =
 350  htmlheader_and_content := !htmlheader_and_content ^ msg ;
 351  outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
 352  outputhtml#set_topline (-1)
 353 ;;
 354
 355 (***********************)
 356 (*       TACTICS       *)
 357 (***********************)
 358
 359 let call_tactic tactic rendering_window () =
 360  let proofw = (rendering_window#proofw : GMathView.math_view) in
 361  let output = (rendering_window#output : GMathView.math_view) in
 362  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 363  let savedproof = !ProofEngine.proof in
 364  let savedgoal  = !ProofEngine.goal in
 365   begin
 366    try
 367     tactic () ;
 368     refresh_sequent proofw ;
 369     refresh_proof output
 370    with
 371       RefreshSequentException e ->
 372        output_html outputhtml
 373         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 374          "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 375        ProofEngine.proof := savedproof ;
 376        ProofEngine.goal := savedgoal ;
 377        refresh_sequent proofw
 378     | RefreshProofException e ->
 379        output_html outputhtml
 380         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 381          "proof: " ^ Printexc.to_string e ^ "</h1>") ;
 382        ProofEngine.proof := savedproof ;
 383        ProofEngine.goal := savedgoal ;
 384        refresh_sequent proofw ;
 385        refresh_proof output
 386     | e ->
 387        output_html outputhtml
 388         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 389        ProofEngine.proof := savedproof ;
 390        ProofEngine.goal := savedgoal ;
 391   end
 392 ;;
 393
 394 let call_tactic_with_input tactic rendering_window () =
 395  let proofw = (rendering_window#proofw : GMathView.math_view) in
 396  let output = (rendering_window#output : GMathView.math_view) in
 397  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 398  let inputt = (rendering_window#inputt : GEdit.text) in
 399  let savedproof = !ProofEngine.proof in
 400  let savedgoal  = !ProofEngine.goal in
 401 (*CSC: Gran cut&paste da sotto... *)
 402   let inputlen = inputt#length in
 403   let input = inputt#get_chars 0 inputlen ^ "\n" in
 404    let lexbuf = Lexing.from_string input in
 405    let curi =
 406     match !ProofEngine.proof with
 407        None -> assert false
 408      | Some (curi,_,_,_) -> curi
 409    in
 410    let uri,metasenv,bo,ty =
 411     match !ProofEngine.proof with
 412        None -> assert false
 413      | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
 414    in
 415    let context =
 416     List.map
 417      (function
 418          Some (n,_) -> Some n
 419        | None -> None)
 420      (match !ProofEngine.goal with
 421          None -> assert false
 422        | Some metano ->
 423           let (_,canonical_context,_) =
 424            List.find (function (m,_,_) -> m=metano) metasenv
 425           in
 426            canonical_context
 427      )
 428    in
 429     try
 430      while true do
 431       match
 432        CicTextualParserContext.main
 433         curi context metasenv CicTextualLexer.token lexbuf
 434       with
 435          None -> ()
 436        | Some (metasenv',expr) ->
 437           ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
 438           tactic expr ;
 439           refresh_sequent proofw ;
 440           refresh_proof output
 441      done
 442     with
 443        CicTextualParser0.Eof ->
 444         inputt#delete_text 0 inputlen
 445      | RefreshSequentException e ->
 446         output_html outputhtml
 447          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 448           "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 449         ProofEngine.proof := savedproof ;
 450         ProofEngine.goal := savedgoal ;
 451         refresh_sequent proofw
 452      | RefreshProofException e ->
 453         output_html outputhtml
 454          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 455           "proof: " ^ Printexc.to_string e ^ "</h1>") ;
 456         ProofEngine.proof := savedproof ;
 457         ProofEngine.goal := savedgoal ;
 458         refresh_sequent proofw ;
 459         refresh_proof output
 460      | e ->
 461         output_html outputhtml
 462          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 463         ProofEngine.proof := savedproof ;
 464         ProofEngine.goal := savedgoal ;
 465 ;;
 466
 467 let call_tactic_with_goal_input tactic rendering_window () =
 468  let module L = LogicalOperations in
 469  let module G = Gdome in
 470   let proofw = (rendering_window#proofw : GMathView.math_view) in
 471   let output = (rendering_window#output : GMathView.math_view) in
 472   let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 473   let savedproof = !ProofEngine.proof in
 474   let savedgoal  = !ProofEngine.goal in
 475    match proofw#get_selection with
 476      Some node ->
 477       let xpath =
 478        ((node : Gdome.element)#getAttributeNS
 479          ~namespaceURI:helmns
 480          ~localName:(G.domString "xref"))#to_string
 481       in
 482        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 483        else
 484         begin
 485          try
 486           match !current_goal_infos with
 487              Some (ids_to_terms, ids_to_father_ids,_) ->
 488               let id = xpath in
 489                tactic (Hashtbl.find ids_to_terms id) ;
 490                refresh_sequent rendering_window#proofw ;
 491                refresh_proof rendering_window#output
 492            | None -> assert false (* "ERROR: No current term!!!" *)
 493          with
 494             RefreshSequentException e ->
 495              output_html outputhtml
 496               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 497                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 498              ProofEngine.proof := savedproof ;
 499              ProofEngine.goal := savedgoal ;
 500              refresh_sequent proofw
 501           | RefreshProofException e ->
 502              output_html outputhtml
 503               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 504                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
 505              ProofEngine.proof := savedproof ;
 506              ProofEngine.goal := savedgoal ;
 507              refresh_sequent proofw ;
 508              refresh_proof output
 509           | e ->
 510              output_html outputhtml
 511               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 512              ProofEngine.proof := savedproof ;
 513              ProofEngine.goal := savedgoal ;
 514         end
 515    | None ->
 516       output_html outputhtml
 517        ("<h1 color=\"red\">No term selected</h1>")
 518 ;;
 519
 520 let call_tactic_with_input_and_goal_input tactic rendering_window () =
 521  let module L = LogicalOperations in
 522  let module G = Gdome in
 523   let proofw = (rendering_window#proofw : GMathView.math_view) in
 524   let output = (rendering_window#output : GMathView.math_view) in
 525   let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 526   let inputt = (rendering_window#inputt : GEdit.text) in
 527   let savedproof = !ProofEngine.proof in
 528   let savedgoal  = !ProofEngine.goal in
 529    match proofw#get_selection with
 530      Some node ->
 531       let xpath =
 532        ((node : Gdome.element)#getAttributeNS
 533          ~namespaceURI:helmns
 534          ~localName:(G.domString "xref"))#to_string
 535       in
 536        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 537        else
 538         begin
 539          try
 540           match !current_goal_infos with
 541              Some (ids_to_terms, ids_to_father_ids,_) ->
 542               let id = xpath in
 543                (* Let's parse the input *)
 544                let inputlen = inputt#length in
 545                let input = inputt#get_chars 0 inputlen ^ "\n" in
 546                 let lexbuf = Lexing.from_string input in
 547                 let curi =
 548                  match !ProofEngine.proof with
 549                     None -> assert false
 550                   | Some (curi,_,_,_) -> curi
 551                 in
 552                 let uri,metasenv,bo,ty =
 553                  match !ProofEngine.proof with
 554                     None -> assert false
 555                   | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
 556                 in
 557                 let context =
 558                  List.map
 559                   (function
 560                       Some (n,_) -> Some n
 561                     | None -> None)
 562                   (match !ProofEngine.goal with
 563                       None -> assert false
 564                     | Some metano ->
 565                        let (_,canonical_context,_) =
 566                         List.find (function (m,_,_) -> m=metano) metasenv
 567                        in
 568                         canonical_context
 569                   )
 570                 in
 571                  begin
 572                   try
 573                    while true do
 574                     match
 575                      CicTextualParserContext.main curi context metasenv
 576                       CicTextualLexer.token lexbuf
 577                     with
 578                        None -> ()
 579                      | Some (metasenv',expr) ->
 580                         ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
 581                         tactic ~goal_input:(Hashtbl.find ids_to_terms id)
 582                          ~input:expr ;
 583                         refresh_sequent proofw ;
 584                         refresh_proof output
 585                    done
 586                   with
 587                      CicTextualParser0.Eof ->
 588                       inputt#delete_text 0 inputlen
 589                  end
 590            | None -> assert false (* "ERROR: No current term!!!" *)
 591          with
 592             RefreshSequentException e ->
 593              output_html outputhtml
 594               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 595                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 596              ProofEngine.proof := savedproof ;
 597              ProofEngine.goal := savedgoal ;
 598              refresh_sequent proofw
 599           | RefreshProofException e ->
 600              output_html outputhtml
 601               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 602                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
 603              ProofEngine.proof := savedproof ;
 604              ProofEngine.goal := savedgoal ;
 605              refresh_sequent proofw ;
 606              refresh_proof output
 607           | e ->
 608              output_html outputhtml
 609               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 610              ProofEngine.proof := savedproof ;
 611              ProofEngine.goal := savedgoal ;
 612         end
 613    | None ->
 614       output_html outputhtml
 615        ("<h1 color=\"red\">No term selected</h1>")
 616 ;;
 617
 618 let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
 619  let module L = LogicalOperations in
 620  let module G = Gdome in
 621   let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in
 622   let outputhtml = (scratch_window#outputhtml : GHtml.xmhtml) in
 623   let savedproof = !ProofEngine.proof in
 624   let savedgoal  = !ProofEngine.goal in
 625    match mmlwidget#get_selection with
 626      Some node ->
 627       let xpath =
 628        ((node : Gdome.element)#getAttributeNS
 629          ~namespaceURI:helmns
 630          ~localName:(G.domString "xref"))#to_string
 631       in
 632        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 633        else
 634         begin
 635          try
 636           match !current_scratch_infos with
 637              (* term is the whole goal in the scratch_area *)
 638              Some (term,ids_to_terms, ids_to_father_ids,_) ->
 639               let id = xpath in
 640                let expr = tactic term (Hashtbl.find ids_to_terms id) in
 641                 let mml = mml_of_cic_term 111 expr in
 642                  scratch_window#show () ;
 643                  scratch_window#mmlwidget#load_tree ~dom:mml
 644            | None -> assert false (* "ERROR: No current term!!!" *)
 645          with
 646           e ->
 647            output_html outputhtml
 648             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 649         end
 650    | None ->
 651       output_html outputhtml
 652        ("<h1 color=\"red\">No term selected</h1>")
 653 ;;
 654
 655 let call_tactic_with_hypothesis_input tactic rendering_window () =
 656  let module L = LogicalOperations in
 657  let module G = Gdome in
 658   let proofw = (rendering_window#proofw : GMathView.math_view) in
 659   let output = (rendering_window#output : GMathView.math_view) in
 660   let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 661   let savedproof = !ProofEngine.proof in
 662   let savedgoal  = !ProofEngine.goal in
 663    match proofw#get_selection with
 664      Some node ->
 665       let xpath =
 666        ((node : Gdome.element)#getAttributeNS
 667          ~namespaceURI:helmns
 668          ~localName:(G.domString "xref"))#to_string
 669       in
 670        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 671        else
 672         begin
 673          try
 674           match !current_goal_infos with
 675              Some (_,_,ids_to_hypotheses) ->
 676               let id = xpath in
 677                tactic (Hashtbl.find ids_to_hypotheses id) ;
 678                refresh_sequent rendering_window#proofw ;
 679                refresh_proof rendering_window#output
 680            | None -> assert false (* "ERROR: No current term!!!" *)
 681          with
 682             RefreshSequentException e ->
 683              output_html outputhtml
 684               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 685                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 686              ProofEngine.proof := savedproof ;
 687              ProofEngine.goal := savedgoal ;
 688              refresh_sequent proofw
 689           | RefreshProofException e ->
 690              output_html outputhtml
 691               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 692                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
 693              ProofEngine.proof := savedproof ;
 694              ProofEngine.goal := savedgoal ;
 695              refresh_sequent proofw ;
 696              refresh_proof output
 697           | e ->
 698              output_html outputhtml
 699               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 700              ProofEngine.proof := savedproof ;
 701              ProofEngine.goal := savedgoal ;
 702         end
 703    | None ->
 704       output_html outputhtml
 705        ("<h1 color=\"red\">No term selected</h1>")
 706 ;;
 707
 708
 709 let intros rendering_window = call_tactic ProofEngine.intros rendering_window;;
 710 let exact rendering_window =
 711  call_tactic_with_input ProofEngine.exact rendering_window
 712 ;;
 713 let apply rendering_window =
 714  call_tactic_with_input ProofEngine.apply rendering_window
 715 ;;
 716 let elimsimplintros rendering_window =
 717  call_tactic_with_input ProofEngine.elim_simpl_intros rendering_window
 718 ;;
 719 let elimtype rendering_window =
 720  call_tactic_with_input ProofEngine.elim_type rendering_window
 721 ;;
 722 let whd rendering_window =
 723  call_tactic_with_goal_input ProofEngine.whd rendering_window
 724 ;;
 725 let reduce rendering_window =
 726  call_tactic_with_goal_input ProofEngine.reduce rendering_window
 727 ;;
 728 let simpl rendering_window =
 729  call_tactic_with_goal_input ProofEngine.simpl rendering_window
 730 ;;
 731 let fold rendering_window =
 732  call_tactic_with_input ProofEngine.fold rendering_window
 733 ;;
 734 let cut rendering_window =
 735  call_tactic_with_input ProofEngine.cut rendering_window
 736 ;;
 737 let change rendering_window =
 738  call_tactic_with_input_and_goal_input ProofEngine.change rendering_window
 739 ;;
 740 let letin rendering_window =
 741  call_tactic_with_input ProofEngine.letin rendering_window
 742 ;;
 743 let ring rendering_window = call_tactic ProofEngine.ring rendering_window;;
 744 let clearbody rendering_window =
 745  call_tactic_with_hypothesis_input ProofEngine.clearbody rendering_window
 746 ;;
 747 let clear rendering_window =
 748  call_tactic_with_hypothesis_input ProofEngine.clear rendering_window
 749 ;;
 750 let fourier rendering_window =
 751  call_tactic ProofEngine.fourier rendering_window
 752 ;;
 753 let rewritesimpl rendering_window =
 754  call_tactic_with_input ProofEngine.rewrite_simpl rendering_window
 755 ;;
 756 let reflexivity rendering_window =
 757  call_tactic ProofEngine.reflexivity rendering_window
 758 ;;
 759 let symmetry rendering_window =
 760  call_tactic ProofEngine.symmetry rendering_window
 761 ;;
 762 let transitivity rendering_window =
 763  call_tactic_with_input ProofEngine.transitivity rendering_window
 764 ;;
 765 let left rendering_window =
 766  call_tactic ProofEngine.left rendering_window
 767 ;;
 768 let right rendering_window =
 769  call_tactic ProofEngine.right rendering_window
 770 ;;
 771 let assumption rendering_window =
 772  call_tactic ProofEngine.assumption rendering_window
 773 ;;
 774 (*
 775 let prova_tatticali rendering_window =
 776  call_tactic ProofEngine.prova_tatticali rendering_window
 777 ;;
 778 *)
 779
 780
 781 let whd_in_scratch scratch_window =
 782  call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
 783   scratch_window
 784 ;;
 785 let reduce_in_scratch scratch_window =
 786  call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch
 787   scratch_window
 788 ;;
 789 let simpl_in_scratch scratch_window =
 790  call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch
 791   scratch_window
 792 ;;
 793
 794
 795
 796 (**********************)
 797 (*   END OF TACTICS   *)
 798 (**********************)
 799
 800 exception OpenConjecturesStillThere;;
 801 exception WrongProof;;
 802
 803 let qed rendering_window () =
 804  match !ProofEngine.proof with
 805     None -> assert false
 806   | Some (uri,[],bo,ty) ->
 807      if
 808       CicReduction.are_convertible []
 809        (CicTypeChecker.type_of_aux' [] [] bo) ty
 810      then
 811       begin
 812        (*CSC: Wrong: [] is just plainly wrong *)
 813        let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in
 814         let
 815          (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
 816           ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
 817         =
 818          Cic2acic.acic_object_of_cic_object proof
 819         in
 820          let mml =
 821           mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
 822          in
 823           (rendering_window#output : GMathView.math_view)#load_tree mml ;
 824           current_cic_infos :=
 825            Some
 826             (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
 827              ids_to_hypotheses)
 828       end
 829      else
 830       raise WrongProof
 831   | _ -> raise OpenConjecturesStillThere
 832 ;;
 833
 834 (*????
 835 let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";;
 836 let dtdname = "/home/tassi/miohelm/helm/dtd/cic.dtd";;
 837 *)
 838 let dtdname = "/projects/helm/V7_mowgli/dtd/cic.dtd";;
 839
 840 let save rendering_window () =
 841  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 842   match !ProofEngine.proof with
 843      None -> assert false
 844    | Some (uri, metasenv, bo, ty) ->
 845       let currentproof =
 846        (*CSC: Wrong: [] is just plainly wrong *)
 847        Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
 848       in
 849        let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
 850         Cic2acic.acic_object_of_cic_object currentproof
 851        in
 852         let xml, bodyxml =
 853          match Cic2Xml.print_object uri ~ids_to_inner_sorts acurrentproof with
 854             xml,Some bodyxml -> xml,bodyxml
 855           | _,None -> assert false
 856         in
 857          Xml.pp ~quiet:true xml (Some prooffiletype) ;
 858          output_html outputhtml
 859           ("<h1 color=\"Green\">Current proof type saved to " ^
 860            prooffiletype ^ "</h1>") ;
 861          Xml.pp ~quiet:true bodyxml (Some prooffile) ;
 862          output_html outputhtml
 863           ("<h1 color=\"Green\">Current proof body saved to " ^
 864            prooffile ^ "</h1>")
 865 ;;
 866
 867 (* Used to typecheck the loaded proofs *)
 868 let typecheck_loaded_proof metasenv bo ty =
 869  let module T = CicTypeChecker in
 870   ignore (
 871    List.fold_left
 872     (fun metasenv ((_,context,ty) as conj) ->
 873       ignore (T.type_of_aux' metasenv context ty) ;
 874       metasenv @ [conj]
 875     ) [] metasenv) ;
 876   ignore (T.type_of_aux' metasenv [] ty) ;
 877   ignore (T.type_of_aux' metasenv [] bo)
 878 ;;
 879
 880 (*CSC: ancora da implementare *)
 881 let load rendering_window () =
 882  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 883  let output = (rendering_window#output : GMathView.math_view) in
 884  let proofw = (rendering_window#proofw : GMathView.math_view) in
 885   try
 886    let uri = UriManager.uri_of_string "cic:/dummy.con" in
 887     match CicParser.obj_of_xml prooffiletype (Some prooffile) with
 888        Cic.CurrentProof (_,metasenv,bo,ty,_) ->
 889         typecheck_loaded_proof metasenv bo ty ;
 890         ProofEngine.proof :=
 891          Some (uri, metasenv, bo, ty) ;
 892         ProofEngine.goal :=
 893          (match metasenv with
 894              [] -> None
 895            | (metano,_,_)::_ -> Some metano
 896          ) ;
 897         refresh_proof output ;
 898         refresh_sequent proofw ;
 899          output_html outputhtml
 900           ("<h1 color=\"Green\">Current proof type loaded from " ^
 901             prooffiletype ^ "</h1>") ;
 902          output_html outputhtml
 903           ("<h1 color=\"Green\">Current proof body loaded from " ^
 904             prooffile ^ "</h1>")
 905      | _ -> assert false
 906   with
 907      RefreshSequentException e ->
 908       output_html outputhtml
 909        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 910         "sequent: " ^ Printexc.to_string e ^ "</h1>")
 911    | RefreshProofException e ->
 912       output_html outputhtml
 913        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 914         "proof: " ^ Printexc.to_string e ^ "</h1>")
 915    | e ->
 916       output_html outputhtml
 917        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 918 ;;
 919
 920 let proveit rendering_window () =
 921  let module L = LogicalOperations in
 922  let module G = Gdome in
 923  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 924   match rendering_window#output#get_selection with
 925     Some node ->
 926      let xpath =
 927       ((node : Gdome.element)#getAttributeNS
 928       (*CSC: OCAML DIVERGE
 929       ((element : G.element)#getAttributeNS
 930       *)
 931         ~namespaceURI:helmns
 932         ~localName:(G.domString "xref"))#to_string
 933      in
 934       if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 935       else
 936        begin
 937         try
 938          match !current_cic_infos with
 939             Some (ids_to_terms, ids_to_father_ids, _, _) ->
 940              let id = xpath in
 941               L.to_sequent id ids_to_terms ids_to_father_ids ;
 942               refresh_proof rendering_window#output ;
 943               refresh_sequent rendering_window#proofw
 944           | None -> assert false (* "ERROR: No current term!!!" *)
 945         with
 946            RefreshSequentException e ->
 947             output_html outputhtml
 948              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 949               "sequent: " ^ Printexc.to_string e ^ "</h1>")
 950          | RefreshProofException e ->
 951             output_html outputhtml
 952              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 953               "proof: " ^ Printexc.to_string e ^ "</h1>")
 954          | e ->
 955             output_html outputhtml
 956              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 957        end
 958   | None -> assert false (* "ERROR: No selection!!!" *)
 959 ;;
 960
 961 let focus rendering_window () =
 962  let module L = LogicalOperations in
 963  let module G = Gdome in
 964  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 965   match rendering_window#output#get_selection with
 966     Some node ->
 967      let xpath =
 968       ((node : Gdome.element)#getAttributeNS
 969       (*CSC: OCAML DIVERGE
 970       ((element : G.element)#getAttributeNS
 971       *)
 972         ~namespaceURI:helmns
 973         ~localName:(G.domString "xref"))#to_string
 974      in
 975       if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 976       else
 977        begin
 978         try
 979          match !current_cic_infos with
 980             Some (ids_to_terms, ids_to_father_ids, _, _) ->
 981              let id = xpath in
 982               L.focus id ids_to_terms ids_to_father_ids ;
 983               refresh_sequent rendering_window#proofw
 984           | None -> assert false (* "ERROR: No current term!!!" *)
 985         with
 986            RefreshSequentException e ->
 987             output_html outputhtml
 988              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 989               "sequent: " ^ Printexc.to_string e ^ "</h1>")
 990          | RefreshProofException e ->
 991             output_html outputhtml
 992              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 993               "proof: " ^ Printexc.to_string e ^ "</h1>")
 994          | e ->
 995             output_html outputhtml
 996              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 997        end
 998   | None -> assert false (* "ERROR: No selection!!!" *)
 999 ;;
1000
1001 exception NoPrevGoal;;
1002 exception NoNextGoal;;
1003
1004 let prevgoal metasenv metano =
1005  let rec aux =
1006   function
1007      [] -> assert false
1008    | [(m,_,_)] -> raise NoPrevGoal
1009    | (n,_,_)::(m,_,_)::_ when m=metano -> n
1010    | _::tl -> aux tl
1011  in
1012   aux metasenv
1013 ;;
1014
1015 let nextgoal metasenv metano =
1016  let rec aux =
1017   function
1018      [] -> assert false
1019    | [(m,_,_)] when m = metano -> raise NoNextGoal
1020    | (m,_,_)::(n,_,_)::_ when m=metano -> n
1021    | _::tl -> aux tl
1022  in
1023   aux metasenv
1024 ;;
1025
1026 let prev_or_next_goal select_goal rendering_window () =
1027  let module L = LogicalOperations in
1028  let module G = Gdome in
1029  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
1030   let metasenv =
1031    match !ProofEngine.proof with
1032       None -> assert false
1033     | Some (_,metasenv,_,_) -> metasenv
1034   in
1035   let metano =
1036    match !ProofEngine.goal with
1037       None -> assert false
1038     | Some m -> m
1039   in
1040    try
1041     ProofEngine.goal := Some (select_goal metasenv metano) ;
1042     refresh_sequent rendering_window#proofw
1043    with
1044       RefreshSequentException e ->
1045        output_html outputhtml
1046         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1047          "sequent: " ^ Printexc.to_string e ^ "</h1>")
1048     | e ->
1049        output_html outputhtml
1050         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1051 ;;
1052
1053 exception NotADefinition;;
1054
1055 let open_ rendering_window () =
1056  let inputt = (rendering_window#inputt : GEdit.text) in
1057  let oldinputt = (rendering_window#oldinputt : GEdit.text) in
1058  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
1059  let output = (rendering_window#output : GMathView.math_view) in
1060  let proofw = (rendering_window#proofw : GMathView.math_view) in
1061   let inputlen = inputt#length in
1062   let input = inputt#get_chars 0 inputlen in
1063    try
1064     let uri = UriManager.uri_of_string ("cic:" ^ input) in
1065      CicTypeChecker.typecheck uri ;
1066      let metasenv,bo,ty =
1067       match CicEnvironment.get_cooked_obj uri with
1068          Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
1069        | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
1070        | Cic.Constant _
1071        | Cic.Variable _
1072        | Cic.InductiveDefinition _ -> raise NotADefinition
1073      in
1074       ProofEngine.proof :=
1075        Some (uri, metasenv, bo, ty) ;
1076       ProofEngine.goal := None ;
1077       refresh_sequent proofw ;
1078       refresh_proof output ;
1079       inputt#delete_text 0 inputlen ;
1080       ignore(oldinputt#insert_text input oldinputt#length)
1081    with
1082       RefreshSequentException e ->
1083        output_html outputhtml
1084         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1085          "sequent: " ^ Printexc.to_string e ^ "</h1>")
1086     | RefreshProofException e ->
1087        output_html outputhtml
1088         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1089          "proof: " ^ Printexc.to_string e ^ "</h1>")
1090     | e ->
1091        output_html outputhtml
1092         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1093 ;;
1094
1095 let state rendering_window () =
1096  let inputt = (rendering_window#inputt : GEdit.text) in
1097  let oldinputt = (rendering_window#oldinputt : GEdit.text) in
1098  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
1099  let output = (rendering_window#output : GMathView.math_view) in
1100  let proofw = (rendering_window#proofw : GMathView.math_view) in
1101   let inputlen = inputt#length in
1102   let input = inputt#get_chars 0 inputlen ^ "\n" in
1103    (* Do something interesting *)
1104    let lexbuf = Lexing.from_string input in
1105     try
1106      while true do
1107       (* Execute the actions *)
1108       match CicTextualParser.main CicTextualLexer.token lexbuf with
1109          None -> ()
1110        | Some expr ->
1111           let _  = CicTypeChecker.type_of_aux' [] [] expr in
1112            ProofEngine.proof :=
1113             Some (UriManager.uri_of_string "cic:/dummy.con",
1114                    [1,[],expr], Cic.Meta (1,[]), expr) ;
1115            ProofEngine.goal := Some 1 ;
1116            refresh_sequent proofw ;
1117            refresh_proof output ;
1118      done
1119     with
1120        CicTextualParser0.Eof ->
1121         inputt#delete_text 0 inputlen ;
1122         ignore(oldinputt#insert_text input oldinputt#length)
1123      | RefreshSequentException e ->
1124         output_html outputhtml
1125          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1126           "sequent: " ^ Printexc.to_string e ^ "</h1>")
1127      | RefreshProofException e ->
1128         output_html outputhtml
1129          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1130           "proof: " ^ Printexc.to_string e ^ "</h1>")
1131      | e ->
1132         output_html outputhtml
1133          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1134 ;;
1135
1136 let check rendering_window scratch_window () =
1137  let inputt = (rendering_window#inputt : GEdit.text) in
1138  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
1139  let output = (rendering_window#output : GMathView.math_view) in
1140  let proofw = (rendering_window#proofw : GMathView.math_view) in
1141   let inputlen = inputt#length in
1142   let input = inputt#get_chars 0 inputlen ^ "\n" in
1143   let curi,metasenv =
1144    match !ProofEngine.proof with
1145       None -> UriManager.uri_of_string "cic:/dummy.con", []
1146     | Some (curi,metasenv,_,_) -> curi,metasenv
1147   in
1148   let context,names_context =
1149    let context =
1150     match !ProofEngine.goal with
1151        None -> []
1152      | Some metano ->
1153         let (_,canonical_context,_) =
1154          List.find (function (m,_,_) -> m=metano) metasenv
1155         in
1156          canonical_context
1157    in
1158     context,
1159     List.map
1160      (function
1161          Some (n,_) -> Some n
1162        | None -> None
1163      ) context
1164   in
1165    let lexbuf = Lexing.from_string input in
1166     try
1167      while true do
1168       (* Execute the actions *)
1169       match
1170        CicTextualParserContext.main curi names_context metasenv
1171         CicTextualLexer.token lexbuf
1172       with
1173          None -> ()
1174        | Some (metasenv',expr) ->
1175           try
1176            let ty  = CicTypeChecker.type_of_aux' metasenv' context expr in
1177             let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
1178 prerr_endline ("### " ^ CicPp.ppterm expr ^ " ==> " ^ CicPp.ppterm ty) ;
1179              scratch_window#show () ;
1180              scratch_window#mmlwidget#load_tree ~dom:mml
1181           with
1182            e ->
1183             print_endline ("? " ^ CicPp.ppterm expr) ;
1184             raise e
1185      done
1186     with
1187        CicTextualParser0.Eof -> ()
1188      | e ->
1189        output_html outputhtml
1190         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1191 ;;
1192
1193 exception NoObjectsLocated;;
1194
1195 let user_uri_choice uris =
1196  let uri =
1197   match uris with
1198      [] -> raise NoObjectsLocated
1199    | [uri] -> uri
1200    | uris ->
1201       let choice =
1202        GToolbox.question_box ~title:"Ambiguous result."
1203         ~buttons:uris ~default:1
1204         "Ambiguous result. Please, choose one."
1205       in
1206        List.nth uris (choice-1)
1207  in
1208   String.sub uri 4 (String.length uri - 4)
1209 ;;
1210
1211 (* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
1212 let get_last_query =
1213  let query = ref "" in
1214   MQueryGenerator.set_confirm_query
1215    (function q -> query := MQueryUtil.text_of_query q ; true) ;
1216   function result -> !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
1217 ;;
1218
1219 let locate rendering_window () =
1220  let inputt = (rendering_window#inputt : GEdit.text) in
1221  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
1222   let inputlen = inputt#length in
1223   let input = inputt#get_chars 0 inputlen in
1224    try
1225     match Str.split (Str.regexp "[ \t]+") input with
1226        [] -> ()
1227      | head :: tail ->
1228         inputt#delete_text 0 inputlen ;
1229         let result = MQueryGenerator.locate head in
1230         let uris =
1231          List.map
1232           (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
1233           result in
1234         let html = (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>") in
1235          output_html outputhtml html ;
1236          let uri' = user_uri_choice uris in
1237           ignore ((inputt#insert_text uri') ~pos:0)
1238    with
1239     e ->
1240      output_html outputhtml
1241       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1242 ;;
1243
1244 let searchPattern rendering_window () =
1245  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
1246  let inputt = (rendering_window#inputt : GEdit.text) in
1247   let inputlen = inputt#length in
1248   let input = inputt#get_chars 0 inputlen in
1249   let level = int_of_string input in
1250   let metasenv =
1251    match !ProofEngine.proof with
1252       None -> assert false
1253     | Some (_,metasenv,_,_) -> metasenv
1254   in
1255    try
1256     match !ProofEngine.goal with
1257        None -> ()
1258      | Some metano ->
1259         let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
1260          let result = MQueryGenerator.searchPattern metasenv ey ty level in
1261          let uris =
1262           List.map
1263            (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
1264            result in
1265          let html =
1266           " <h1>Backward Query: </h1>" ^
1267           " <h2>Levels: </h2> " ^
1268            MQueryGenerator.string_of_levels
1269             (MQueryGenerator.levels_of_term metasenv ey ty) "<br>" ^
1270            " <pre>" ^ get_last_query result ^ "</pre>"
1271          in
1272           output_html outputhtml html ;
1273           let uris',exc =
1274            let rec filter_out =
1275             function
1276                [] -> [],""
1277              | uri::tl ->
1278                 let tl',exc = filter_out tl in
1279                  try
1280                   if ProofEngine.can_apply (term_of_uri uri) then
1281                    uri::tl',exc
1282                   else
1283                    tl',exc
1284                  with
1285                   e ->
1286                    let exc' =
1287                     "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
1288                      uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
1289                    in
1290                     tl',exc'
1291            in
1292             filter_out uris
1293           in
1294            let html' =
1295             " <h1>Objects that can actually be applied: </h1> " ^
1296             String.concat "<br>" uris' ^ exc ^
1297             " <h1>Number of false matches: " ^
1298              string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
1299             " <h1>Number of good matches: " ^
1300              string_of_int (List.length uris') ^ "</h1>"
1301            in
1302             output_html outputhtml html' ;
1303             let uri' = user_uri_choice uris' in
1304              inputt#delete_text 0 inputlen ;
1305              ignore ((inputt#insert_text uri') ~pos:0)
1306     with
1307      e ->
1308       output_html outputhtml
1309        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1310 ;;
1311
1312 let choose_selection
1313      (mmlwidget : GMathView.math_view) (element : Gdome.element option)
1314 =
1315  let module G = Gdome in
1316   let rec aux element =
1317    if element#hasAttributeNS
1318        ~namespaceURI:helmns
1319        ~localName:(G.domString "xref")
1320    then
1321      mmlwidget#set_selection (Some element)
1322    else
1323       match element#get_parentNode with
1324          None -> assert false
1325        (*CSC: OCAML DIVERGES!
1326        | Some p -> aux (new G.element_of_node p)
1327        *)
1328        | Some p -> aux (new Gdome.element_of_node p)
1329   in
1330    match element with
1331      Some x -> aux x
1332    | None   -> mmlwidget#set_selection None
1333 ;;
1334
1335 (* STUFF TO BUILD THE GTK INTERFACE *)
1336
1337 (* Stuff for the widget settings *)
1338
1339 let export_to_postscript (output : GMathView.math_view) () =
1340  output#export_to_postscript ~filename:"output.ps" ();
1341 ;;
1342
1343 let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
1344  button_set_kerning button_set_transparency button_export_to_postscript
1345  button_t1 ()
1346 =
1347  let is_set = button_t1#active in
1348   output#set_font_manager_type
1349    (if is_set then `font_manager_t1 else `font_manager_gtk) ;
1350   if is_set then
1351    begin
1352     button_set_anti_aliasing#misc#set_sensitive true ;
1353     button_set_kerning#misc#set_sensitive true ;
1354     button_set_transparency#misc#set_sensitive true ;
1355     button_export_to_postscript#misc#set_sensitive true ;
1356    end
1357   else
1358    begin
1359     button_set_anti_aliasing#misc#set_sensitive false ;
1360     button_set_kerning#misc#set_sensitive false ;
1361     button_set_transparency#misc#set_sensitive false ;
1362     button_export_to_postscript#misc#set_sensitive false ;
1363    end
1364 ;;
1365
1366 let set_anti_aliasing output button_set_anti_aliasing () =
1367  output#set_anti_aliasing button_set_anti_aliasing#active
1368 ;;
1369
1370 let set_kerning output button_set_kerning () =
1371  output#set_kerning button_set_kerning#active
1372 ;;
1373
1374 let set_transparency output button_set_transparency () =
1375  output#set_transparency button_set_transparency#active
1376 ;;
1377
1378 let changefont output font_size_spinb () =
1379  output#set_font_size font_size_spinb#value_as_int
1380 ;;
1381
1382 let set_log_verbosity output log_verbosity_spinb () =
1383  output#set_log_verbosity log_verbosity_spinb#value_as_int
1384 ;;
1385
1386 class settings_window (output : GMathView.math_view) sw
1387  button_export_to_postscript selection_changed_callback
1388 =
1389  let settings_window = GWindow.window ~title:"GtkMathView settings" () in
1390  let vbox =
1391   GPack.vbox ~packing:settings_window#add () in
1392  let table =
1393   GPack.table
1394    ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
1395    ~border_width:5 ~packing:vbox#add () in
1396  let button_t1 =
1397   GButton.toggle_button ~label:"activate t1 fonts"
1398    ~packing:(table#attach ~left:0 ~top:0) () in
1399  let button_set_anti_aliasing =
1400   GButton.toggle_button ~label:"set_anti_aliasing"
1401    ~packing:(table#attach ~left:0 ~top:1) () in
1402  let button_set_kerning =
1403   GButton.toggle_button ~label:"set_kerning"
1404    ~packing:(table#attach ~left:1 ~top:1) () in
1405  let button_set_transparency =
1406   GButton.toggle_button ~label:"set_transparency"
1407    ~packing:(table#attach ~left:2 ~top:1) () in
1408  let table =
1409   GPack.table
1410    ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
1411    ~border_width:5 ~packing:vbox#add () in
1412  let font_size_label =
1413   GMisc.label ~text:"font size:"
1414    ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
1415  let font_size_spinb =
1416   let sadj =
1417    GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
1418   in
1419    GEdit.spin_button
1420     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
1421  let log_verbosity_label =
1422   GMisc.label ~text:"log verbosity:"
1423    ~packing:(table#attach ~left:0 ~top:1) () in
1424  let log_verbosity_spinb =
1425   let sadj =
1426    GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
1427   in
1428    GEdit.spin_button
1429     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
1430  let hbox =
1431   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1432  let closeb =
1433   GButton.button ~label:"Close"
1434    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1435 object(self)
1436  method show = settings_window#show
1437  initializer
1438   button_set_anti_aliasing#misc#set_sensitive false ;
1439   button_set_kerning#misc#set_sensitive false ;
1440   button_set_transparency#misc#set_sensitive false ;
1441   (* Signals connection *)
1442   ignore(button_t1#connect#clicked
1443    (activate_t1 output button_set_anti_aliasing button_set_kerning
1444     button_set_transparency button_export_to_postscript button_t1)) ;
1445   ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
1446   ignore(button_set_anti_aliasing#connect#toggled
1447    (set_anti_aliasing output button_set_anti_aliasing));
1448   ignore(button_set_kerning#connect#toggled
1449    (set_kerning output button_set_kerning)) ;
1450   ignore(button_set_transparency#connect#toggled
1451    (set_transparency output button_set_transparency)) ;
1452   ignore(log_verbosity_spinb#connect#changed
1453    (set_log_verbosity output log_verbosity_spinb)) ;
1454   ignore(closeb#connect#clicked settings_window#misc#hide)
1455 end;;
1456
1457 (* Scratch window *)
1458
1459 class scratch_window outputhtml =
1460  let window =
1461   GWindow.window ~title:"MathML viewer" ~border_width:2 () in
1462  let vbox =
1463   GPack.vbox ~packing:window#add () in
1464  let hbox =
1465   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1466  let whdb =
1467   GButton.button ~label:"Whd"
1468    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1469  let reduceb =
1470   GButton.button ~label:"Reduce"
1471    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1472  let simplb =
1473   GButton.button ~label:"Simpl"
1474    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1475  let scrolled_window =
1476   GBin.scrolled_window ~border_width:10
1477    ~packing:(vbox#pack ~expand:true ~padding:5) () in
1478  let mmlwidget =
1479   GMathView.math_view
1480    ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
1481 object(self)
1482  method outputhtml = outputhtml
1483  method mmlwidget = mmlwidget
1484  method show () = window#misc#hide () ; window#show ()
1485  initializer
1486   ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
1487   ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
1488   ignore(whdb#connect#clicked (whd_in_scratch self)) ;
1489   ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
1490   ignore(simplb#connect#clicked (simpl_in_scratch self))
1491 end;;
1492
1493 (* Main window *)
1494
1495 class rendering_window output proofw (label : GMisc.label) =
1496  let window =
1497   GWindow.window ~title:"MathML viewer" ~border_width:2 () in
1498  let hbox0 =
1499   GPack.hbox ~packing:window#add () in
1500  let vbox =
1501   GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1502  let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
1503  let scrolled_window0 =
1504   GBin.scrolled_window ~border_width:10
1505    ~packing:(vbox#pack ~expand:true ~padding:5) () in
1506  let _ = scrolled_window0#add output#coerce in
1507  let hbox1 =
1508   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1509  let settingsb =
1510   GButton.button ~label:"Settings"
1511    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1512  let button_export_to_postscript =
1513   GButton.button ~label:"export_to_postscript"
1514   ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1515  let qedb =
1516   GButton.button ~label:"Qed"
1517    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1518  let saveb =
1519   GButton.button ~label:"Save"
1520    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1521  let loadb =
1522   GButton.button ~label:"Load"
1523    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1524  let closeb =
1525   GButton.button ~label:"Close"
1526    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1527  let hbox2 =
1528   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1529  let proveitb =
1530   GButton.button ~label:"Prove It"
1531    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1532  let focusb =
1533   GButton.button ~label:"Focus"
1534    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1535  let prevgoalb =
1536   GButton.button ~label:"<"
1537    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1538  let nextgoalb =
1539   GButton.button ~label:">"
1540    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1541  let oldinputt = GEdit.text ~editable:false ~width:400 ~height:180
1542    ~packing:(vbox#pack ~padding:5) () in
1543  let hbox4 =
1544   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1545  let stateb =
1546   GButton.button ~label:"State"
1547    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1548  let openb =
1549   GButton.button ~label:"Open"
1550    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1551  let checkb =
1552   GButton.button ~label:"Check"
1553    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1554  let locateb =
1555   GButton.button ~label:"Locate"
1556    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1557  let searchpatternb =
1558   GButton.button ~label:"SearchPattern"
1559    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1560  let inputt = GEdit.text ~editable:true ~width:400 ~height: 100
1561    ~packing:(vbox#pack ~padding:5) () in
1562  let vbox1 =
1563   GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1564  let scrolled_window1 =
1565   GBin.scrolled_window ~border_width:10
1566    ~packing:(vbox1#pack ~expand:true ~padding:5) () in
1567  let _ = scrolled_window1#add proofw#coerce in
1568  let hbox3 =
1569   GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1570  let exactb =
1571   GButton.button ~label:"Exact"
1572    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1573  let introsb =
1574   GButton.button ~label:"Intros"
1575    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1576  let applyb =
1577   GButton.button ~label:"Apply"
1578    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1579  let elimsimplintrosb =
1580   GButton.button ~label:"ElimSimplIntros"
1581    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1582  let elimtypeb =
1583   GButton.button ~label:"ElimType"
1584    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1585  let whdb =
1586   GButton.button ~label:"Whd"
1587    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1588  let reduceb =
1589   GButton.button ~label:"Reduce"
1590    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1591  let simplb =
1592   GButton.button ~label:"Simpl"
1593    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1594  let foldb =
1595   GButton.button ~label:"Fold"
1596    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1597  let cutb =
1598   GButton.button ~label:"Cut"
1599    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1600  let changeb =
1601   GButton.button ~label:"Change"
1602    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1603  let hbox4 =
1604   GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1605  let letinb =
1606   GButton.button ~label:"Let ... In"
1607    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1608  let ringb =
1609   GButton.button ~label:"Ring"
1610    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1611  let clearbodyb =
1612   GButton.button ~label:"ClearBody"
1613    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1614  let clearb =
1615   GButton.button ~label:"Clear"
1616    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1617  let fourierb =
1618   GButton.button ~label:"Fourier"
1619    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1620  let rewritesimplb =
1621   GButton.button ~label:"RewriteSimpl ->"
1622    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1623  let reflexivityb =
1624   GButton.button ~label:"Reflexivity"
1625    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1626  let symmetryb =
1627   GButton.button ~label:"Symmetry"
1628    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1629  let transitivityb =
1630   GButton.button ~label:"Transitivity"
1631    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1632  let hbox5 =
1633   GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1634  let leftb =
1635   GButton.button ~label:"Left"
1636    ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
1637  let rightb =
1638   GButton.button ~label:"Right"
1639    ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
1640  let assumptionb =
1641   GButton.button ~label:"Assumption"
1642    ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
1643 (*
1644  let prova_tatticalib =
1645   GButton.button ~label:"Prova_tatticali"
1646    ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
1647 *)
1648  let outputhtml =
1649   GHtml.xmhtml
1650    ~source:"<html><body bgColor=\"white\"></body></html>"
1651    ~width:400 ~height: 200
1652    ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5)
1653    ~show:true () in
1654  let scratch_window = new scratch_window outputhtml in
1655 object(self)
1656  method outputhtml = outputhtml
1657  method oldinputt = oldinputt
1658  method inputt = inputt
1659  method output = (output : GMathView.math_view)
1660  method proofw = (proofw : GMathView.math_view)
1661  method show = window#show
1662  initializer
1663   button_export_to_postscript#misc#set_sensitive false ;
1664
1665   (* signal handlers here *)
1666   ignore(output#connect#selection_changed
1667    (function elem -> proofw#unload ; choose_selection output elem)) ;
1668   ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
1669   ignore(closeb#connect#clicked (fun _ -> GMain.Main.quit ())) ;
1670   let settings_window = new settings_window output scrolled_window0
1671    button_export_to_postscript (choose_selection output) in
1672   ignore(settingsb#connect#clicked settings_window#show) ;
1673   ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
1674   ignore(qedb#connect#clicked (qed self)) ;
1675   ignore(saveb#connect#clicked (save self)) ;
1676   ignore(loadb#connect#clicked (load self)) ;
1677   ignore(proveitb#connect#clicked (proveit self)) ;
1678   ignore(focusb#connect#clicked (focus self)) ;
1679   ignore(prevgoalb#connect#clicked (prev_or_next_goal prevgoal self)) ;
1680   ignore(nextgoalb#connect#clicked (prev_or_next_goal nextgoal self)) ;
1681   ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
1682   ignore(stateb#connect#clicked (state self)) ;
1683   ignore(openb#connect#clicked (open_ self)) ;
1684   ignore(checkb#connect#clicked (check self scratch_window)) ;
1685   ignore(locateb#connect#clicked (locate self)) ;
1686   ignore(searchpatternb#connect#clicked (searchPattern self)) ;
1687   ignore(exactb#connect#clicked (exact self)) ;
1688   ignore(applyb#connect#clicked (apply self)) ;
1689   ignore(elimsimplintrosb#connect#clicked (elimsimplintros self)) ;
1690   ignore(elimtypeb#connect#clicked (elimtype self)) ;
1691   ignore(whdb#connect#clicked (whd self)) ;
1692   ignore(reduceb#connect#clicked (reduce self)) ;
1693   ignore(simplb#connect#clicked (simpl self)) ;
1694   ignore(foldb#connect#clicked (fold self)) ;
1695   ignore(cutb#connect#clicked (cut self)) ;
1696   ignore(changeb#connect#clicked (change self)) ;
1697   ignore(letinb#connect#clicked (letin self)) ;
1698   ignore(ringb#connect#clicked (ring self)) ;
1699   ignore(clearbodyb#connect#clicked (clearbody self)) ;
1700   ignore(clearb#connect#clicked (clear self)) ;
1701   ignore(fourierb#connect#clicked (fourier self)) ;
1702   ignore(rewritesimplb#connect#clicked (rewritesimpl self)) ;
1703   ignore(reflexivityb#connect#clicked (reflexivity self)) ;
1704   ignore(symmetryb#connect#clicked (symmetry self)) ;
1705   ignore(transitivityb#connect#clicked (transitivity self)) ;
1706   ignore(leftb#connect#clicked (left self)) ;
1707   ignore(rightb#connect#clicked (right self)) ;
1708   ignore(assumptionb#connect#clicked (assumption self)) ;
1709 (*
1710   ignore(prova_tatticalib#connect#clicked (prova_tatticali self)) ;
1711 *)
1712   ignore(introsb#connect#clicked (intros self)) ;
1713   Logger.log_callback :=
1714    (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
1715 end;;
1716
1717 (* MAIN *)
1718
1719 let rendering_window = ref None;;
1720
1721 let initialize_everything () =
1722  let module U = Unix in
1723   let output = GMathView.math_view ~width:350 ~height:280 ()
1724   and proofw = GMathView.math_view ~width:400 ~height:275 ()
1725   and label = GMisc.label ~text:"gTopLevel" () in
1726     let rendering_window' =
1727      new rendering_window output proofw label
1728     in
1729      rendering_window := Some rendering_window' ;
1730      rendering_window'#show () ;
1731      GMain.Main.main ()
1732 ;;
1733
1734 let _ =
1735  if !usedb then
1736   begin
1737 (*
1738    Mqint.init "dbname=helm" ;
1739 *)
1740    Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ;
1741    CicTextualParser0.set_locate_object
1742     (function id ->
1743       let result = MQueryGenerator.locate id in
1744       let uris =
1745        List.map
1746         (function uri,_ ->
1747           wrong_xpointer_format_from_wrong_xpointer_format' uri
1748         ) result in
1749       let html =
1750        (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>")
1751       in
1752        begin
1753         match !rendering_window with
1754            None -> assert false
1755          | Some rw -> output_html rw#outputhtml html ;
1756        end ;
1757        let uri =
1758         match uris with
1759            [] ->
1760             (match
1761               (GToolbox.input_string ~title:"Unknown input"
1762                ("No URI matching \"" ^ id ^ "\" found. Please enter its URI"))
1763              with
1764                 None -> None
1765               | Some uri -> Some ("cic:" ^ uri)
1766             )
1767          | [uri] -> Some uri
1768          | _ ->
1769            let choice =
1770             GToolbox.question_box ~title:"Ambiguous input."
1771              ~buttons:uris ~default:1 "Ambiguous input. Please, choose one."
1772            in
1773             if choice > 0 then
1774              Some (List.nth uris (choice - 1))
1775             else
1776              (* No choice from the user *)
1777              None
1778        in
1779         match uri with
1780            Some uri' -> Some (cic_textual_parser_uri_of_uri uri')
1781          | None -> None
1782     )
1783   end ;
1784  ignore (GtkMain.Main.init ()) ;
1785  initialize_everything () ;
1786  if !usedb then Mqint.close ();
1787 ;;