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