# HG changeset patch # User wenzelm # Date 1368303659 -7200 # Node ID 972c4f42fd525857369c89fd1938321e8397abb3 # Parent a5265222d6e6c18c7b786fcf44b9cfd67fd77985# Parent 916c7fe684e3e5400452abad15a3839d71a5626e merged diff -r a5265222d6e6 -r 972c4f42fd52 bin/isabelle-process --- a/bin/isabelle-process Sat May 11 16:00:24 2013 +0200 +++ b/bin/isabelle-process Sat May 11 22:20:59 2013 +0200 @@ -31,7 +31,6 @@ echo " -S secure mode -- disallow critical operations" echo " -T ADDR startup process wrapper, with socket address" echo " -W IN:OUT startup process wrapper, with input/output fifos" - echo " -X startup PGIP interaction mode" echo " -e MLTEXT pass MLTEXT to the ML session" echo " -f pass 'Session.finish();' to the ML session" echo " -m MODE add print mode for output" @@ -64,14 +63,13 @@ SECURE="" WRAPPER_SOCKET="" WRAPPER_FIFOS="" -PGIP="" MLTEXT="" MODES="" TERMINATE="" READONLY="" NOWRITE="" -while getopts "IPST:W:Xe:fm:qruw" OPT +while getopts "IPST:W:e:fm:qruw" OPT do case "$OPT" in I) @@ -89,9 +87,6 @@ W) WRAPPER_FIFOS="$OPTARG" ;; - X) - PGIP=true - ;; e) MLTEXT="$MLTEXT $OPTARG" ;; @@ -226,8 +221,6 @@ [ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}" [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}" MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";" -elif [ -n "$PGIP" ]; then - MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;" elif [ -n "$PROOFGENERAL" ]; then MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;" elif [ "$ISAR" = true ]; then diff -r a5265222d6e6 -r 972c4f42fd52 lib/ProofGeneral/README --- a/lib/ProofGeneral/README Sat May 11 16:00:24 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,21 +0,0 @@ -This directory contains a PGIP configuration file "pgip_isar.xml" -which can be used to configure the behaviour of PGIP-aware interfaces -communicating in PGIP with Isabelle. The current version of this file -is incomplete and experimental, because interfaces that use it are -still in development. - -Note that Isabelle does not do anything with the configurations -specified here, it simply passes the file directly on to the interface -during startup inside an XML message. - -The file which is sent can be overridden at run time by setting the -variable ISABELLE_PGIPCONFIG to point to an alternative location. - -The file here is valid wrt to the RELAX compact schema in "pgip.rnc". - -See http://proofgeneral.inf.ed.ac.uk/kit for more details of the -Proof General Kit project. - - - -- David Aspinall, Sep 2005. - diff -r a5265222d6e6 -r 972c4f42fd52 lib/ProofGeneral/pgip.rnc --- a/lib/ProofGeneral/pgip.rnc Sat May 11 16:00:24 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1063 +0,0 @@ -# -# RELAX NG Schema for PGIP, the Proof General Interface Protocol -# -# Authors: David Aspinall, LFCS, University of Edinburgh -# Christoph Lüth, University of Bremen -# -# Status: Prototype. -# -# For additional commentary, see accompanying commentary document available at -# http://proofgeneral.inf.ed.ac.uk/Kit/docs/commentary.pdf -# -# Advertised version: 2.0 -# -# Contents -# ======== -# -# 0. Prelude -# 1. Top-level -# 2. Component Control messages -# 3. Display Commands -# 4. Prover Configuration -# 5. Interface Configuration -# 6. Prover Control -# 7. Proof script markup and proof control -# -# -# =============================================================================== -# -# Note on datatypes. (see e.g. http://books.xmlschemata.org/relaxng): -# -# token : any string possibly with spaces, but spaces are normalised/collapsed -# (i.e. tokenised). Same as XML Schema xs:token -# string : any string, whitespaces preserved. Same as XML Schema xs:string -# (NB: attributes are normalised by XML 1.0 parsers so -# spaces/newlines must be quoted) -# text : text nodes/mixed content (whitespace may be lost in mixed content) -# -# So: attributes should usually be tokens or more restrictive; (sometimes: strings for printing) -# element contents may be string (preserving whitespace), token (tokenising), -# or text (which may contain further nodes). - -# ============================================================================== -# 0. Prelude -# ============================================================================== - -include "pgml.rnc" # include PGML grammar - -name_attr = attribute name { token } # names are user-level textual identifiers (space-collapsed) -thyname_attr = attribute thyname { token } # names for theories (special case of name) -thmname_attr = attribute thmname { token } # names for theorems (special case of name) - -datetime_attr = - attribute datetime { xsd:dateTime } # CCYY-MM-DDHH:MM:SS plus timezone info -url_attr = attribute url { xsd:anyURI } # URLs (often as "file:///localfilename.extn") -dir_attr = attribute dir { string } # Unix-style directory name (no final slash) - -systemdata_attr = - attribute systemdata { token }? # system-specific data (useful for "stateless" RPC) - -objname = token # an identifier name (convention: any characters except semi-colon) -objnames = token # sequence of names in an attribute: semi-colon separated - -#objnames = string # A sequence of objnames -#termobjname = string { pattern = "[^;]+;" } # unfortunately these declarations don't -#objnames = objname | (termobjname, objname) -#objnames = objname+ # work with the RNC->DTD tool trang - - -# ============================================================================== -# 1. Top-level Messages/documents -# ============================================================================== - -start = pgip # Single message - | pgips # A log of messages between components - | displayconfig # displayconfig as a standalone element - | pgipconfig # pgipconfig as a standalone element - | pgipdoc # A proof script document - -pgip = element pgip { # A PGIP packet contains: - pgip_attrs, # - attributes with header information; - (toprovermsg | todisplaymsg | # - a message with one of four channel types - fromprovermsg | fromdisplaymsg - | internalmsg ) - } - -pgips = element pgips { pgip+ } - -pgip_attrs = - attribute tag { token }?, # message tag, e.g. name of origin component (diagnostic) - attribute id { token }, # (unique) session id of this component - attribute destid { token }?, # session id of destination component - attribute class { pgip_class }, # general categorization of message - attribute refid { token }?, # component id this message responds to (usually destid) - attribute refseq { xsd:positiveInteger }?, # message sequence this message responds to - attribute seq { xsd:positiveInteger } # sequence number of this message - -pgip_class = "pg" # message sent TO proof general broker (e.g. FROM proof assistant). - | "pa" # message sent TO the proof assistant/other component - | "pd" # message sent TO display/front-end components - -toprovermsg = # Messages sent to the prover (class "pa"): - proverconfig # query Prover configuration, triggering interface configuration - | provercontrol # control some aspect of Prover - | improperproofcmd # issue a proof command - | improperfilecmd # issue a file command - | properproofcmd # [ NB: not strictly needed: input PGIP processing not expected ] - | properfilecmd # [ NB: not strictly needed: input PGIP processing not expected ] - | proofctxt # issue a context command - -fromprovermsg = # Messages from the prover to PG (class "pg"): - kitconfig # messages to configure the interface - | proveroutput # output messages from the prover, usually display in interface - | fileinfomsg # information messages concerning file-system access / prover state - -todisplaymsg = # Messages sent to display components (class "pd"): - brokermsg # status reports from broker - | dispmsg # display commands - # - Further, all fromprovermsg can be relayed to display - -fromdisplaymsg = # Messages sent from display components (class "pg"): - dispcmd # display messages - | brokercontrol # messages controlling broker & prover processes - # - Further, all toprovermsg to be relayed to prover - -# =========================================================================== -# 2. Component Control -# =========================================================================== - -# -# Idea: - broker knows how to manage some components (inc provers) as child processes, -# communicate via pipes. Configured by a fixed PGIP config file read on startup. -# - other components may connect to running broker -# -# TODO: - describe startup protocol for component connecting to to running broker dynamically. - -# This is the element contained in the configuration file read by the -# broker on startup. -pgipconfig = element pgipconfig { componentspec* } - -componentspec = - element componentspec { - componentid_attr, # Unique identifier for component class - componentname_attr, # Textual name of component class - componenttype, # Type of component: prover, display, auxiliary - startupattrs, # Describing startup behaviour - systemattrs, # System attributes for component - componentconnect # How to connect to component - } - -componentid_attr = attribute componentid { token } -componentname_attr = attribute componentname { token } - -componenttype = element componenttype { - provercomponent - | displaycomponent - # | filehandlercomponent - | parsercomponent - | othercomponent } - -provercomponent = element provercomponent { empty } -displaycomponent = element displaycomponent { attribute active { xsd:boolean}? } -parsercomponent = element parsercomponent { componentid_attr } -othercomponent = element othercomponent { empty } - -componentconnect = - componentsubprocess | componentsocket | connectbyproxy - -componentsubprocess = - element syscommand { string } -componentsocket = - (element host { token }, element port { xsd:positiveInteger }) -connectbyproxy = - (element proxy { attribute host { token } # Host to connect to - , attribute connect { - "rsh" | "ssh" # Launch proxy via RSH or SSH, needs - # authentication - | "server" # connect to running proxy on given port - }? - , attribute user { token } ? # user to connect as with RSH/SSH - , attribute path { token } ? # path of pgipkit on remote - , attribute port { xsd:positiveInteger } ? # port to connect to running proxy - , componentconnect - }) - -# Attributes describing when to start the component. -startupattrs = - attribute startup { # what to do on broker startup: - "boot" | # always start this component (default with displays) - "manual" | # start manually (default with provers) - "ignore" # never start this component - }? - -# System attributes describing behaviour of component. -systemattrs = ( - attribute timeout { xsd:integer }? # timeout for communications - , attribute sync { xsd:boolean }? # whether to wait for ready - , attribute nestedgoals { xsd:boolean}? # Does prover allow nested goals? - ) - -# Control commands from display to broker -brokercontrol = - launchprover # Launch a new prover - | exitprover # Request to terminate a running prover - | restartprover # Request to restart/reset a running prover - | proversquery # Query about known provers, running provers - | shutdownbroker # Ask broker to exit (should be wary of this!) - | brokerstatusquery # Ask broker for status report - | pgipconfig # Send config to broker - -provername_attr = attribute provername { provername } -provername = token - -proverid_attr = attribute proverid { proverid } -proverid = token - -launchprover = element launchprover { componentid_attr } -exitprover = element exitprover { proverid_attr } -restartprover = element restartprover { proverid_attr } -proversquery = element proversavailable { empty } -brokerstatusquery = element brokerstatusquery { empty } -shutdownbroker = element shutdownbroker { attribute force { xsd:boolean }? } - -# Control messages from broker to interface -brokermsg = - brokerstatus # response to brokerstatusquery: - | proveravailmsg # announce new prover is available - | newprovermsg # new prover has started - | proverstatemsg # prover state has changed (busy/ready/exit) - -brokerstatus = element brokerstatus - { knownprovers, runningprovers, brokerinformation } - -knownprover = element knownprover { componentid_attr, provername } -runningprover = element runningprover { componentid_attr, proverid_attr, provername } - -knownprovers = element knownprovers { knownprover* } -runningprovers = element runningprovers { runningprover* } -brokerinformation = element brokerinformation { string } - -proveravailmsg = element proveravailable { provername_attr, - componentid_attr } -newprovermsg = element proverstarted { proverid_attr - , componentid_attr - , provername_attr - } -proverstatemsg = element proverstate { - proverid_attr, provername_attr, - attribute proverstate {proverstate} } - -proverstate = ("ready" | "busy" | "exitus") - -# FIXME: This only allows provers to be available which are configured. -# In the long run, we want to change configurations while running. - - -# =========================================================================== -# 3. Display Commands -# =========================================================================== - -# Messages exchanged between broker and display - - -dispcmd = dispfilecmd | dispobjcmd # display commands go from display to broker -dispmsg = dispfilemsg | dispobjmsg # display messages go from broker to display - - -dispfilecmd = - loadparsefile # parse and load file - | newfilewith # create new source file with given text - | dispopenfile # open (or create) new file - | savefile # save opened file - | discardfile # discard changes to opened file - -dispfilemsg = - newfile # announce creation of new file (in response to load/open) - | filestatus # announce change in status of file in broker - -# unique identifier of loaded files -srcid_attr = attribute srcid { token } - -loadparsefile = element loadparsefile { url_attr, proverid_attr } -newfilewith = element newfilewith { url_attr, proverid_attr, string } -dispopenfile = element dispopenfile { url_attr, - proverid_attr, - attribute overwrite { xsd:boolean }?} -savefile = element savefile { srcid_attr, - url_attr? } -discardfile = element discardfile { srcid_attr } - -newfile = element newfile { proverid_attr, srcid_attr, url_attr } -filestatus = element filestatus { proverid_attr, srcid_attr, newstatus_attr, url_attr?, - datetime_attr} - -newstatus_attr = attribute newstatus { "saved" | "changed" | "discarded" } - -dispobjcmd = - setobjstate # request of change of state - | editobj # request edit operation of objects - | createobj # request creation of new objects -# Suggested May 06: probably add re-load flags instead -# | reloadobjs # request relisting of all objects - | inputcmd # process the command (generated by an input event) - | interruptprover # send interrupt or kill signal to prover - -dispobjmsg = element dispobjmsg { - newobj+ # new objects have been created - | delobj+ # objects have been deleted - | replaceobjs # objects are being replaced - | objectstate+ # objects have changed state - } - -newobj = element newobj { - proverid_attr, - srcid_attr, - objid_attr, - attribute objposition { objid } ?, - objtype_attr ?, - attribute objparent { objid }?, - attribute objstate { objstate }, - # FIXME: would like to include metainfo here - # as (properscriptcmd, metainfo*) | unparseable - (properscriptcmd | unparseable) } - -replaceobjs = element replaceobjs { - srcid_attr, - attribute replacedfrom { objid }? , - attribute replacedto { objid }?, - delobj*, # actually, either of delobj or - newobj* } # newobj can be empty but not both. - -delobj = element delobj { proverid_attr, srcid_attr, objid_attr } - -objectstate = element objstate - { proverid_attr, srcid_attr, objid_attr, - attribute newstate {objstate} } - -setobjstate = element setobjstate - { objid_attr, attribute newstate {objstate} } - -editobj = element editobj { srcid_attr ?, - attribute editfrom { objid }?, - attribute editto { objid }?, - string } -createobj = element createobj { srcid_attr ?, - attribute objposition { objid }?, - string } - -# Suggested May 06: probably add re-load flags instead -# reloadobjs = element reloadobjs { srcid_attr } - -inputcmd = element inputcmd { improper_attr, string } -improper_attr = attribute improper { xsd:boolean } - -interruptprover = element interruptprover - { interruptlevel_attr, proverid_attr } - -interruptlevel_attr = attribute interruptlevel { "interrupt" | "stop" | "kill" } - -objid_attr = attribute objid { objid } -objid = token - -objstate = - ( "unparseable" | "parsed" | "being_processed" | "processed" | "outdated" ) - - -# ============================================================================== -# 4. Prover Configuration -# ============================================================================== - -proverconfig = - askpgip # what version of PGIP do you support? - | askpgml # what version of PGML do you support? - | askconfig # tell me about objects and operations - | askprefs # what preference settings do you offer? - | setpref # please set this preference value - | getpref # please tell me this preference value - - - -prefcat_attr = attribute prefcategory { token } # e.g. "expert", "internal", etc. - # could be used for tabs in dialog - -askpgip = element askpgip { empty } -askpgml = element askpgml { empty } -askconfig = element askconfig { empty } -askprefs = element askprefs { prefcat_attr? } -setpref = element setpref { name_attr, prefcat_attr?, pgipvalue } -getpref = element getpref { name_attr, prefcat_attr? } - - - -# ============================================================================== -# 5. Interface Configuration -# ============================================================================== - -kitconfig = - usespgip # I support PGIP, version .. - | usespgml # I support PGML, version .. - | pgmlconfig # configure PGML symbols - | proverinfo # Report assistant information - | hasprefs # I have preference settings ... - | prefval # the current value of a preference is - | displayconfig # configure the following object types and operations - | setids # inform the interface about some known objects - | addids # add some known identifiers - | delids # retract some known identifers - | idvalue # display the value of some identifier - | menuadd # add a menu entry - | menudel # remove a menu entry - -# version reporting -version_attr = attribute version { token } -usespgml = element usespgml { version_attr } -usespgip = element usespgip { version_attr - , activecompspec - } - -# These data from the component spec which an active component can override, or which -# components initiating contact with the broker (e.g. incoming socket connections). -# There are some restrictions: if we start a tool, the componentid and the type must be the -# same as initially specified. -activecompspec = ( componentid_attr? # unique identifier of component class - , componentname_attr? # Textual name of this component (overrides initial spec) - , componenttype? # Type of component - , systemattrs # system attributes - , acceptedpgipelems? # list of accepted elements - ) - - -acceptedpgipelems = element acceptedpgipelems { singlepgipelem* } - -singlepgipelem = element pgipelem { - attribute async { xsd:boolean }?, # true if this command supported asynchronously (deflt false) - # (otherwise part of usual ready/sync stream) - attribute attributes { text }?, # comma-separated list of supported optional attribute names - # useful for: times attribute - text } # the unadorned name of the PGIP element (*not* an element) - -# PGML configuration -pgmlconfig = element pgmlconfig { pgmlconfigure+ } - -# Types for config settings: corresponding data values should conform to canonical -# representation for corresponding XML Schema 1.0 Datatypes. -# -# In detail: -# pgipnull = empty -# pgipbool = xsd:boolean = true | false -# pgipint = xsd:integer = (-)?(0-9)+ (canonical: no leading zeroes) -# pgipstring = string = -# pgipchoice = cf xs:choice = type1 | type2 | ... | typen - -pgiptype = pgipnull | pgipbool | pgipint | pgipstring | pgipchoice | pgipconst - -pgipnull = element pgipnull { descr_attr?, empty } -pgipbool = element pgipbool { descr_attr?, empty } -pgipint = element pgipint { min_attr?, max_attr?, descr_attr?, empty } -min_attr = attribute min { xsd:integer } -max_attr = attribute max { xsd:integer } -pgipstring = element pgipstring { descr_attr?, empty } -pgipconst = element pgipconst { name_attr, descr_attr? } - # FIXME: Temporary fix because Isabelle does it wrong -- should be empty } -pgipchoice = element pgipchoice { pgiptype+ } - -# Notes on pgipchoice: -# 1. Choices must not be nested (i.e. must not contain other choices) -# 2. The description attributes for pgipbool, pgipint, pgipstring and pgipconst -# are for use with pgipchoice: they can be used as a user-visible label -# when representing the choice to the user (e.g. in a pull-down menu). -# 3. A pgipchoice should have an unambiguous representation as a string. That means -# all constants in the choice must have different names, and a choice must not -# contain more than one each of pgipint, pgipstring and pgipbool. - -pgipvalue = string - -icon = element icon { xsd:base64Binary } # image data for an icon - -# The default value of a preference as a string (using the unambiguous -# conversion to string mentioned above). A string value will always be quoted -# to distinguish it from constants or integers. -default_attr = attribute default { token } - -# Description of a choice. If multi-line, first line is short tip. -descr_attr = attribute descr { string } - -# icons for preference recommended size: 32x32 -# top level preferences: may be used in dialog for preference setting -# object preferences: may be used as an "emblem" to decorate -# object icon (boolean preferences with default false, only) -haspref = element haspref { - name_attr, descr_attr?, - default_attr?, icon?, - pgiptype -} - - - -hasprefs = element hasprefs { prefcat_attr?, haspref* } - -prefval = element prefval { name_attr, pgipvalue } - -# menu items (incomplete, FIXME) -path_attr = attribute path { token } - -menuadd = element menuadd { path_attr?, name_attr?, opn_attr? } -menudel = element menudel { path_attr?, name_attr? } -opn_attr = attribute operation { token } - - -# Display configuration information: -# basic prover information, lexical structure of files, -# an icon for the prover, help documents, and the -# objects, types, and operations for building proof commands. - -# NB: the following object types have a fixed interpretation -# in PGIP: -# "identifier": an identifier in the identifier syntax -# "comment": an arbitrary sequence of characters -# "theorem": a theorem name or text -# "theory" : a theory name or text -# "file" : a file name - -displayconfig = - element displayconfig { - welcomemsg?, icon?, helpdoc*, lexicalstructure*, - objtype*, opn* } - -objtype = element objtype { name_attr, descr_attr?, icon?, contains*, hasprefs? } - -objtype_attr = attribute objtype { token } # the name of an objtype -contains = element contains { objtype_attr, empty } # a container for other objtypes - -opn = element opn { - name_attr, - descr_attr?, - inputform?, # FIXME: can maybe remove this? - opsrc*, # FIXME: incompat change wanted: have list of source elts, not spaces - optrg, - opcmd, - improper_attr? } - -opsrc = - element opsrc { - name_attr?, # %name as an alternative to %number - selnumber_attr?, # explicit number for %number, the nth item selected - prompt_attr?, # prompt in form or tooltip in template - listwithsep_attr?, # list of args of this type with given separator - list { token* } } # source types: a space separated list - # FIXME incompat change wanted: just have one source here - # FIXME: need to add optional pgiptype - -listwithsep_attr = attribute listwithsep { token } -selnumber_attr = attribute selnumber { xsd:positiveInteger } -prompt_attr = attribute prompt { string } - -optrg = - element optrg { token }? # single target type, empty for proof command -opcmd = - element opcmd { string } # prover command, with printf-style "%1"-args - # (whitespace preserved here: literal text) - -# interactive operations - require some input -inputform = element inputform { field+ } - -# a field has a PGIP config type (int, string, bool, choice(c1...cn)) and a name; under that -# name, it will be substituted into the command Ex. field name=number opcmd="rtac %1 %number" - -field = element field { - name_attr, pgiptype, - element prompt { string } -} - -# identifier tables: these list known items of particular objtype. -# Might be used for completion or menu selection, and inspection. -# May have a nested structure (but objtypes do not). - -setids = element setids { idtable* } # (with an empty idtable, clear table) -addids = element addids { idtable* } -delids = element delids { idtable* } - -# give value of some identifier (response to showid; same values returned) -idvalue = element idvalue - { thyname_attr?, name_attr, objtype_attr, pgmltext } - -idtable = element idtable { context_attr?, objtype_attr, identifier* } -identifier = element identifier { token } - -context_attr = attribute context { token } # parent identifier (context) - -# prover information: -# name, instance (e.g. in case of major parameter of invocation); -# description, version, homepage, welcome message, docs available -proverinfo = element proverinfo - { name_attr, version_attr?, instance_attr?, - descr_attr?, url_attr?, filenameextns_attr?, -## TEMP: these elements are duplicated in displayconfig, as they're -## moving there. - welcomemsg?, icon?, helpdoc*, lexicalstructure* } - -instance_attr = attribute instance { token } - -welcomemsg = element welcomemsg { string } - -# helpdoc: advertise availability of some documentation, given a canonical -# name, textual description, and URL or viewdoc argument. -# -helpdoc = element helpdoc { name_attr, descr_attr, url_attr?, token } # token string is arg to "viewdoc" - -filenameextns_attr = attribute filenameextns { xsd:NMTOKENS } # space-separated extensions sans "." - -# lexical structure of proof texts -lexicalstructure = - element lexicalstructure { - keyword*, - stringdelimiter*, - escapecharacter?, - commentdelimiter*, - identifiersyntax? - } - -keyword = element keyword { - attribute word { token }, - shorthelp?, - longhelp? } - -shorthelp = element shorthelp { string } # one-line (tooltip style) help -longhelp = element longhelp { string } # multi-line help - -stringdelimiter = element stringdelimiter { token } # should be a single char - -# The escape character is used to escape strings and other special characters - in most languages it is \ -escapecharacter = element escapecharacter { token } # should be a single char - -commentdelimiter = element commentdelimiter { - attribute start { token }, - attribute end { token }?, - empty - } - - -# syntax for ids: id = initial allowed* or id = allowed+ if initial empty -identifiersyntax = element identifiersyntax { - attribute initialchars { token }?, - attribute allowedchars { token } -} - -# ============================================================================== -# 6. Prover Control -# ============================================================================== - -provercontrol = - proverinit # reset prover to its initial state - | proverexit # exit prover - | startquiet # stop prover sending proof state displays, non-urgent messages - | stopquiet # turn on normal proof state & message displays - | pgmlsymbolson # activate use of symbols in PGML output (input always understood) - | pgmlsymbolsoff # deactivate use of symbols in PGML output - | setproverflag # set/clear a standard control flag (supersedes above) - -proverinit = element proverinit { empty } -proverexit = element proverexit { empty } -startquiet = element startquiet { empty } # DEPRECATED -stopquiet = element stopquiet { empty } # DEPRECATED -pgmlsymbolson = element pgmlsymbolson { empty } # DEPRECATED -pgmlsymbolsoff = element pgmlsymbolsoff { empty } # DEPRECATED - -setproverflag = element setproverflag { flagname_attr, - attribute value { xsd:boolean } } -flagname_attr = - attribute flagname { "quiet" - | "pgmlsymbols" - | "metainfo:thmdeps" - } - -# General prover output/responses - -# Prover output has an otional proverid_attribute. This is set by the broker when relaying -# prover output to displays. When producing output, provers can and should not set this -# attribute. - -proveroutput = - ready # prover is ready for input - | cleardisplay # prover requests a display area to be cleared - | proofstate # prover outputs the proof state - | normalresponse # prover outputs some display - | errorresponse # prover indicates an error/warning/debug condition, with message - | scriptinsert # some text to insert literally into the proof script - | metainforesponse # prover outputs some other meta-information to interface - | parseresult # results of a request (see later) - -ready = element ready { empty } - -displayarea = "status" # a status line - | "message" # the message area (e.g. response buffer, perhaps swapped into view) - | "display" # the main display area (e.g. goals buffer, usually persistent) - | token # prover-specified window name - -cleardisplay = - element cleardisplay { - proverid_attr?, - attribute area { - displayarea | "all" } } - - -proofstate = - element proofstate { proverid_attr?, pgml } - -messagecategory = # attribution of message - "internal" # - internal debug message (interface should usually hide) - | "information" # - user-level debug/info message (interface may hide) - | "tracing" # - user-level "tracing" message (possibly voluminous) - -normalresponse = - element normalresponse { - proverid_attr?, # if no proverid, assume message is from broker - attribute area { displayarea }, - attribute messagecategory { messagecategory }?, # optional extra category (e.g. tracing/debug) - attribute urgent { xsd:boolean }?, # message should be brought to users attention - pgmltext -} - -## Error messages: these are different from ordinary messages in that -## they indicate an error condition in the prover, with a notion -## of fatality and (optionally) a location. The interface may collect these -## messages in a log, display in a modal dialog, or in the specified -## display area if one is given -## -## Error responses are also taken to indicate failure of a command to be processed, but only in -## the special case of a response with fatality "fatal". If any errorresponse with -## fatality=fatal is sent before , the PGIP command which triggered the message is -## considered to have failed. If the command is a scripting command, it will not be added to -## the successfully processed part of the document. A "nonfatal" error also indicates some -## serious problem with the sent command, but it is not considered to have failed. This is the -## ordinary response for - -errorresponse = - element errorresponse { - proverid_attr?, # ... as above ... - attribute area { displayarea }?, - attribute fatality { fatality }, - location_attrs, - pgmltext - } - -fatality = # degree of error conditions: - "info" # - info message - | "warning" # - warning message - | "nonfatal" # - error message, recovered and state updated - | "fatal" # - error message, command has failed - | "panic" # - shutdown condition, component exits (interface may show message) - | "log" # - system-level log message (interface does not show message; written to log file) - | "debug" # - system-level debug message (interface may show message; written to log file) - -# attributes describing a file location (for error messages, etc) -location_attrs = - attribute location_descr { string }?, - attribute location_url { xsd:anyURI }?, - attribute locationline { xsd:positiveInteger }?, - attribute locationcolumn { xsd:positiveInteger }?, - attribute locationcharacter { xsd:positiveInteger }?, - attribute locationlength { xsd:positiveInteger }? - -# instruction to insert some literal text into the document -scriptinsert = element scriptinsert { proverid_attr?, metavarid_attr?, string } - - -# metainformation is an extensible place to put system-specific information - -value = element value { name_attr?, text } # generic value holder [ deprecated: use metainfo ] -metainfo = element metainfo { name_attr?, text } # generic info holder - -metainforesponse = - element metainforesponse { - proverid_attr?, - attribute infotype { token }, # categorization of data - (value | metainfo)* } # data values/text - - -# ============================================================================== -# 7. Proof script markup and proof control -# ============================================================================== - -# properproofcmds are purely markup on native proof script (plain) text -properproofcmd = - opengoal # open a goal in ambient context - | proofstep # a specific proof command (perhaps configured via opcmd) - | closegoal # complete & close current open proof (succeeds iff proven, may close nested pf) - | giveupgoal # close current open proof, retaining attempt in script (Isar oops) - | postponegoal # close current open proof, record as proof obl'n (Isar sorry) - | comment # a proof script comment; text probably ignored by prover - | doccomment # a proof script document comment; text maybe processed by prover - | whitespace # a whitespace comment; text ignored by prover - | spuriouscmd # command ignored for undo, e.g. "print x", could be pruned from script - | badcmd # a command which should not be stored in the script (e.g. an improperproofcmd) - | litcomment # a PGIP literate comment (never passed to prover) - | pragma # a document generating instruction (never passed to prover) - -# improperproofcmds are commands which are never stored in the script -improperproofcmd = - dostep # issue a properproofcmd (without passing in markup) - | undostep # undo the last proof step issued in currently open goal - | redostep # redo the last undone step issued in currently open goal (optionally supported) - | abortgoal # give up on current open proof, close proof state, discard history - | forget # forget a theorem (or named target), outdating dependent theorems - | restoregoal # re-open previously postponed proof, outdating dependent theorems - -# In future we may allow input to contain markup; for now it is treated uniformly as plain text. - -opengoal = element opengoal { display_attr?, thmname_attr?, string } # FIXME: add objprefval -proofstep = element proofstep { display_attr?, name_attr?, objtype_attr?, string } -closegoal = element closegoal { display_attr?, string } -giveupgoal = element giveupgoal { display_attr?, string } -postponegoal = element postponegoal { display_attr?, string } -comment = element comment { display_attr?, string } -doccomment = element doccomment { display_attr?, string } -whitespace = element whitespace { display_attr?, string } - -display_attr = attribute nodisplay { xsd:boolean } # whether to display in documentation - -spuriouscmd = element spuriouscmd { string } # no semantic effect (e.g. print) -badcmd = element badcmd { string } # illegal in script (e.g. undo) -nonscripting = element nonscripting { string } # non-scripting text (different doc type) - -litcomment = element litcomment { format_attr?, (text | directive)* } -directive = element directive { (proofctxt,pgml) } -format_attr = attribute format { token } - -pragma = showhidecode | setformat -showhidecode = element showcode { attribute show { xsd:boolean } } -setformat = element setformat { format_attr } - -dostep = element dostep { string } -undostep = element undostep { times_attr? } -redostep = element redostep { times_attr? } -abortgoal = element abortgoal { empty } -forget = element forget { thyname_attr?, name_attr?, objtype_attr? } -restoregoal = element restoregoal { thmname_attr } - -times_attr = attribute times { xsd:positiveInteger } - -# empty objprefval element is used for object prefs in script markup -objprefval = element objprefval { name_attr, val_attr, empty } -val_attr = attribute value { token } - - - - -# ======================================================= -# Inspecting the proof context, etc. - -# NB: ids/refs/parent: work in progress, liable to change. - -proofctxt = - askids # tell me about identifiers (given objtype in a theory) - | askrefs # tell me about dependencies (references) of an identifier -# | askparent # tell me the container for some identifier - | showid # print the value of some object - | askguise # tell me about the current state of the prover - | parsescript # parse a raw proof script into proofcmds - | showproofstate # (re)display proof state (empty if outside a proof) - | showctxt # show proof context - | searchtheorems # search for theorems (prover-specific arguments) - | setlinewidth # set line width for printing - | viewdoc # request some on-line help (prover-specific arg) - -askids = element askids { thyname_attr?, objtype_attr? } - # Note that thyname_attr is *required* for certain objtypes (e.g. theorem). - # This is because otherwise the list is enormous. - # Perhaps we should make thyname_attr obligatory? - # With a blank entry (i.e. thyname="") allowed for listing theories, or for when - # you really do want to see everything (could be a shell-style glob) - - -# askids: container -> identifiers contained within -# askparent: identifier + type + context -> container -# askrers: identifier + type + context -> identifiers which are referenced -# -askrefs = element askrefs { url_attr?, thyname_attr?, objtype_attr?, name_attr? } -# TODO: maybe include guises here as indication of reference point. -# setrefs in reply to askrefs only really needs identifiers, but it's nice to -# support voluntary information too. -setrefs = element setrefs { url_attr?, thyname_attr?, objtype_attr?, name_attr?, idtable*, fileurl* } -fileurl = element fileurl { url_attr } -# telldeps = element telldeps { thyname_attr?, objtype_attr, name_attr?, identifier* } -# Idea: for a theory dependency we return a single file (URL), the containing file. -# for a file dependency we return urls of parent files, -# for theorem dependency we return theory -# for term dependency we return definition (point in file) - - -showid = element showid { thyname_attr?, objtype_attr, name_attr } - -askguise = element askguise { empty } - -showproofstate = element showproofstate { empty } -showctxt = element showctxt { empty } -searchtheorems = element searchtheorems { string } -setlinewidth = element setlinewidth { xsd:positiveInteger } -viewdoc = element viewdoc { token } - - -# ======================================================= -# Proof script documents and parsing proof scripts - -# A PGIP document is a sequence of script commands, each of which -# may have meta information attached. -properscriptcmdmetainfo = properscriptcmd, metainfo* -pgipdoc = element pgipdoc { properscriptcmdmetainfo* } - - -# NB: parsing needs only be supported for "proper" proof commands, -# which may appear in proof texts. The groupdelimiters are purely -# markup hints to the interface for display structure on concrete syntax. -# The location attributes can be used by the prover in to -# generate error messages for particular locations; they can be used -# in to pass position information back to the display, -# particularly in the case of (re-)parsing only part of a file. -# The parsing component MUST return the same location attributes -# (and system data attribute) that was passed in. - -parsescript = element parsescript - { location_attrs, systemdata_attr, string } - -parseresult = element parseresult { location_attrs, systemdata_attr, - singleparseresult* } - -# Really we'd like parsing to return properscriptcmdmetainfo as a single -# result (and similarly for newobj). -# Unfortunately, although this is an XML-transparent extension, it -# messes up the Haskell schema-fixed code rather extensively, so for -# now we just treat metainfo at the same level as the other results, -# although it should only appear following a properscriptcmd. - -singleparseresult = properscriptcmd | metainfo | unparseable | errorresponse - -unparseable = element unparseable { string } -properscriptcmd = properproofcmd | properfilecmd | groupdelimiter - - - - -groupdelimiter = openblock | closeblock -openblock = element openblock { - name_attr?, objtype_attr?, - metavarid_attr?, positionid_attr?, - fold_attr?, indent_attr? } -closeblock = element closeblock { empty } - -# -metavarid_attr = attribute metavarid { token } -positionid_attr = attribute positionid { token } -fold_attr = attribute fold { xsd:boolean } -indent_attr = attribute indent { xsd:integer } - - -# ======================================================= -# Theory/file handling - -properfilecmd = # (NB: properfilecmds are purely markup on proof script text) - opentheory # begin construction of a new theory. - | theoryitem # a step in a theory (e.g. declaration/definition of type/constant). - | closetheory # complete construction of the currently open theory - -improperfilecmd = - doitem # issue a proper file command (without passing in markup) - | undoitem # undo last step (or named item) in theory construction - | redoitem # redo last step (or named item) in theory construction (optionally supported) - | aborttheory # abort currently open theory - | retracttheory # retract a named theory - | openfile # signal a file is being opened for constructing a proof text interactively - | closefile # close the currently open file, suggesting it has been processed - | abortfile # unlock a file, suggesting it hasn't been processed - | loadfile # load (i.e. process directly) a file possibly containing theory definition(s) - | retractfile # retract a given file (including all contained theories) - | changecwd # change prover's working directory (or load path) for files - | systemcmd # system (other) command, parsed internally - -fileinfomsg = - informfileloaded # prover informs interface a particular file is loaded - | informfileretracted # prover informs interface a particular file is outdated - | informguise # prover informs interface about current state - -opentheory = element opentheory { thyname_attr, parentnames_attr?, string } -closetheory = element closetheory { string } -theoryitem = element theoryitem { name_attr?, objtype_attr?, string } # FIXME: add objprefval - -doitem = element doitem { string } -undoitem = element undoitem { name_attr?, objtype_attr?, times_attr? } -redoitem = element redoitem { name_attr?, objtype_attr?, times_attr? } -aborttheory = element aborttheory { empty } -retracttheory = element retracttheory { thyname_attr } - -parentnames_attr = attribute parentnames { objnames } - - -# Below, url_attr will often be a file URL. We assume for now that -# the prover and interface are running on same filesystem. -# - -openfile = element openfile { url_attr } # notify begin reading from given file -closefile = element closefile { empty } # notify currently open file is complete -abortfile = element abortfile { empty } # notify currently open file is discarded -loadfile = element loadfile { url_attr } # ask prover to read file directly -retractfile = element retractfile { url_attr } # ask prover to retract file -changecwd = element changecwd { url_attr } # ask prover to change current working dir - -# this one not yet implemented, but would be handy. Perhaps could be -# locatethy/locatefile instead. -#locateobj = element locateobj { name_attr, objtype_attr } # ask prover for file defining obj - -informfileloaded = element informfileloaded { completed_attr?, - url_attr } # prover indicates a processed file -informfileretracted = element informfileretracted { completed_attr?, - url_attr } # prover indicates an undone file -informfileoutdated = element informfileoutdated { completed_attr?, - url_attr } # prover indicates an outdated file - -informfilelocation = element informfilelocation { url_attr } # response to locateobj - -completed_attr = attribute completed { xsd:boolean } # false if not completed (absent=>true) - # (the prover is requesting a lock) - - - -informguise = - element informguise { - element guisefile { url_attr }?, - element guisetheory { thyname_attr }?, - element guiseproof { thmname_attr?, proofpos_attr? }? - } - -proofpos_attr = attribute proofpos { xsd:nonNegativeInteger } - -systemcmd = element systemcmd { string } # "shell escape", arbitrary prover command! - -# ============================================================================== -# 8. Internal messages: only used between communicating brokers. -# ============================================================================== -internalmsg = launchcomp | stopcomp | registercomp | compstatus - -launchcomp = element launchcomponent { componentspec } - # request to start an instance of this component remotely -stopcomp = element stopcomponent { attribute sessionid { token } } - # request to stop component with this session id remotely - -registercomp = element registercomponent { activecompspec } - # component has been started successfully -compstatus = element componentstatus { componentstatus_attr # status - , componentid_attr? # component id (for failure) - , element text { string }? # user-visible error message - , element info { string }? # Additional info for log files. - } - # component status: failed to start, or exited - -componentstatus_attr = attribute status { ("fail" # component failed to start - |"exit" # component exited - )} - -# Local variables: -# fill-column: 95 -# End: -# ============================================================================== -# end of `pgip.rnc'. - diff -r a5265222d6e6 -r 972c4f42fd52 lib/ProofGeneral/pgip_isar.xml --- a/lib/ProofGeneral/pgip_isar.xml Sat May 11 16:00:24 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,252 +0,0 @@ - - - - - Welcome to Isabelle/Isar 2007. - - - - iVBORw0KGgoAAAANSUhEUgAAACAAAAAgCAIAAAD8GO2jAAAHG0lEQVRIx7VW - WY9cRxU+p6ru0tvtnp7NmRl7PBqPPU5sB8l2FgS2EwVkeEFEQYp4gggJeIEn - JB4RfwQeeEFikTAIBHFMYiFsBi9x7FnaM+Oe1bP29HZv33ur6hwe2pqMLGOk - oJzHKlV95/vqnPMVMjN8niHgcw71/O00TfFAAMBBxkKI7uJnBNBaR1FkrQUA - KaUQAgCsNWmaErHjOEEQOI7zzLP7wP+DQRSuLyz8Oo5rAoVyPACUIn4w89Aa - U+4dv3DhR4cOnXg+CfV8faKwtblxt9FYIiLf99NUB0FuqbrKzEnCcdz57I/M - zMyMQgLbI0cOM+mxscNad4hSZsvMlgyRfaoID77W8xgwc5qmQgilXEuir6/P - dR1jALgLDIDARPu3P0elZwAQUavVImIphVRKSn9rawuRNzbWmckSAAAypLrT - 6bS11lLKg+k/VVpPAxhjWq22tRYRARjRQxAry9WLb7z1cG4OpWAmBCDgOG4t - LlbqddnTU/R9Rynf97O+72ezWdd19zHwoIha6zAMrSVEZKY0TZeq8w/nflav - L/m+SmKNQgTF3PTMLhEYA9c/hImRnuFR38lASrZYzL766ndeeeWdfD6/T0sd - VAYAlHIqlZXp6eWHlUeVyuLq2jrZei6T6etNSqWO72E2oLm5xN1j2lAvaVts - bTsVkTuetyfae3tZZlBK/VeJpJQAfO2D6Q+uzrZb2tqccke++Nouw2Od1pst - aoZkt1LXQW9ElF+WQcHV9200bcia1HAu3zcyMul5HiJ20xVCqP30u0sAQMz1 - ersTpwgYuI2jo3NKCqnyjisQpTGkDdVqnTA0UWLi1Cpg6RpjOJspBEFZCGGt - SVNNZKVUan+qhGHIzEQ2m3UvXDjfU/K3d5rLyw/IUq4YuK6/vbUJiEIKY1Vt - LwUAJm4nrAznJAODMZZZWGvTNO1WFxGpg/VjjCEiRIqidrW6niYaEMkCEzmO - ywAIwPZJ+TMxALCFpuFBydZSrbY1f/8TBzLSy0glHUcJgZ9KpJQCAK1TBKhU - lodeGDg5OTo7d8cyWquHRw5HUbO2V38yUJlRAFm2hi1zbHFn3uDS1p/++fOP - yr1+Pj84Nj557vyJt76uAMBa28398fru1NTMR9fvbW3vbWzu3r47I6U9f5aN - tY1mvafUF7bDVJsnLfykn9Vmamb/uvuT44MiwNS04412DLC0WGk2mhNvXlYA - UKs1pqYqV9+/dffuQr3eabVb1hCikCrjsmcItBFRmFQfzQtgRGRiZgYEJqhG - YGTxdBnHz79cHh2++ds/H5sY3V1Y+nsj6s/lVVeWf91c/OUvbiyv1DodTBIj - MHB8BczaRJ24Uauxo/TO9hZZJIESusMIyHJzhV5MsBSECPLK1ZtHRwaPTo4P - nzy2WqmykMX+AcdxFAAQG2P1iYnhO3dng8IIM6Q6MiYSQgmhrvzxUiG/PTzc - GBrWQ4NhJies5bU1c3hZHW25BtkCOIiBI9bWNocnJ27+7i8JEQiRKQTMrIi4 - UMi0Wq2+3j5LOk6aREZKx/dLAhWx1To0ZrhapdnZ3URXfe8TKcPdR/qnx/o9 - T7gCETE0tBh2Qku3qmteJ807jpfLB/39RCQAuFDwlRLZTDYIAmYrUDLZUy8e - Hh/vMzrK+KU42Ys628Sk5EhPM2dW7KmCZ5gjY+upaWqz2kkiSyjEb6Zm10hi - vnjqja+cufgmAChEzOf8wcHy9Mz06JGh+w8qDNzXW0o1HRrom56eT9OQyOy3 - y+sjA5dPT8ZJuvKwmiap5zppnFhmAvT87A/ee69Xx/353Jlvf9f1PGZWAFAs - 5cbHX1hYeFzI+8wkpVco5IOC/3hzi5gEEzMxm679NZqtf99cyfne6PGxQiF7 - /NyZv/3q93Z9GxGk533tG2+XBga6rsDM1loFAOVy8M63zhVLYqna6unJh6Eu - FfOfPJg9fWqSmRio21yIjGiFlIAijNOZe7Oe64RRbFKtGQiEdD0/n0MUiE8c - N5vNKkSUUk5MjIyNHdrcrF19f/DatdmB/qDe7F1d3UZEZkYUUopCITs0VDp7 - YggWb+tGPWk1kji5f2faRSQUTiZ76Xs/dP3M/tcJEX3fxy4Ra4kZrLVaJ41G - dONG5cofpqrVnXaYMCkh4qGh4EtfPvnuu5d6e4tJu7V2786jf3y4/eDjaGdb - Wb2O7sXv//gLX73c/T51vTOTybiui8xMRNZaRGGMYSYhJJFtNNq3bs1fvz67 - slwfGMh88+3Xz549JqXsmkn3SGt7a+3j2+3lR+Wzrx156bQQQimllJJSfmrU - +5bJzMYYIkZEIRAAtDZa09raThBkyuWgK5cQAoABGBEBkIiIGACIrFLScZz9 - q5/hyftIB1wImAkREMW+SRERInSHd/eFmJmZlHKkFAfTlVJho9HI5XJPwf6f - EUWdOO4gimIx+A/pRoFAWyKheQAAAABJRU5ErkJggg== - - - tutorial - logics-HOL - isar-overview - isar-ref - ref - system - - - - Begin theory or proof - End theory or proof - " - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - R0lGODlhJgAgAIQAAP////r6+uDg4Nra2tnZ2fn5+WFhYUJCQkFBQWBgYMnO - 91xq6K208wsg3XiD7OTm+0FR5CY54Pb29t3d3dfX119fX/T09NbW1tjY2AAA - AAAAAAAAAAAAAAAAAAAAAAAAACH+FUNyZWF0ZWQgd2l0aCBUaGUgR0lNUAAh - +QQBCgAfACwAAAAAJgAgAAAFnCAgjmRpnqgYCAPhvnAsz7BQAIJxIHzv/8Cg - LyHA6YTI5I8IWLVo0Gjtlqpar9istqRYLBTbMIDRaDDEW7IZrVWf2VYGw1F2 - yBkP+KnM77/1Jm6AcWV/gyeChyiJioGFjYiPkCWMkyKVlpiTmpBqEJYlEWUR - XgugDBCjDnmgrZMSExQUUrQ0NgADFUq7SUy5vMBATBYDFxi1yFMAIQA7 - - - - - R0lGODlhJgAgAIQAAP////r6+uDg4Nra2tnZ2fn5+WFhYUJCQkFBQWBgYOTm - +62080FR5Asg3SY54Fxq6MnO95Kc73iD7Pb29t3d3dfX119fX/T09NbW1tjY - 2AAAAAAAAAAAAAAAAAAAAAAAACH+FUNyZWF0ZWQgd2l0aCBUaGUgR0lNUAAh - +QQBCgAfACwAAAAAJgAgAAAFsyAgjmRpnqgYCAPhvnAsz7BQAIJxIHzv/8Cg - LyHA6YTI5I8IWLVo0Gjtlqpar9istqRYeL9exbaqYDTOaPRijFI40vDGmm16 - NB74NwOPh9C5DWIidn9VERIkb4UpEYIiZ4tZkJFWEA0MlFYLd5lVmw+dKZ8k - fqEim4GnoKYAlndiDIisAG9ppawSaauzALkNsrzBwsPEIxMUFRVSyzQ2AAMW - StJJTNDT10BMFwMYGczfUwAhADs= - - - - - - - - - - - identifier - theory - theory - theory %name imports %imports begin - -end - - - - - Input a name: - Input a term: - - - - - - Attributes: - - - lemma %attributes %name : "%term" -sorry - - - - - - theorem - - declare %1 [simp] - - - - theorem - - declare %1 [simp del] - - - - theorem - term - theorem - %1 [OF %2] - - - - - - - Input a term: - - - term - term %term - - - - - ruleset - apply (rule %1) - - - ruleset - apply (erule %1) - - - ruleset - apply (drule %1) - - - - - - - - diff -r a5265222d6e6 -r 972c4f42fd52 lib/ProofGeneral/pgml.rnc --- a/lib/ProofGeneral/pgml.rnc Sat May 11 16:00:24 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,79 +0,0 @@ -# -# RELAX NG Schema for PGML, the Proof General Markup Language -# -# Authors: David Aspinall, LFCS, University of Edinburgh -# Christoph Lueth, University of Bremen -# -# Status: Complete, prototype. -# -# For additional commentary, see accompanying commentary document -# (available at http://proofgeneral.inf.ed.ac.uk/kit) -# -# Advertised version: 1.0 -# - -pgml_version_attr = attribute version { xsd:NMTOKEN } - -pgml = - element pgml { - pgml_version_attr?, - (statedisplay | termdisplay | information | warning | error)* - } - -termitem = action | nonactionitem -nonactionitem = term | pgmltype | atom | sym - -pgml_mixed = text | termitem | statepart - -pgml_name_attr = attribute name { text } - -kind_attr = attribute kind { text } -systemid_attr = attribute systemid { text } - -statedisplay = - element statedisplay { - pgml_name_attr?, kind_attr?, systemid_attr?, - pgml_mixed* - } - -pgmltext = element pgmltext { (text | termitem)* } - -information = element information { pgml_name_attr?, kind_attr?, pgmltext } - -warning = element warning { pgml_name_attr?, kind_attr?, pgmltext } -error = element error { pgml_name_attr?, kind_attr?, pgmltext } -statepart = element statepart { pgml_name_attr?, kind_attr?, pgmltext } -termdisplay = element termdisplay { pgml_name_attr?, kind_attr?, pgmltext } - -pos_attr = attribute pos { text } - -term = element term { pos_attr?, kind_attr?, pgmltext } - -# maybe combine this with term and add extra attr to term? -pgmltype = element type { kind_attr?, pgmltext } - -action = element action { kind_attr?, (text | nonactionitem)* } - -fullname_attr = attribute fullname { text } -atom = element atom { kind_attr?, fullname_attr?, text } - - -## Symbols -## -## Element sym can be rendered in three alternative ways, -## in descending preference order: -## -## 1) the PGML symbol given by the name attribute -## 2) the text content of the SYM element, if non-empty -## 3) one of the previously configured text alternatives advertised -## by the component who produced this output. -## -symname_attr = attribute name { token } # names must be [a-zA-Z][a-zA-Z0-9]+ -sym = element sym { symname_attr, text } - - -pgmlconfigure = symconfig # inform symbol support (I/O) for given sym - -textalt = attribute alt { text } # text alternative for given sym - -symconfig = element symconfig { symname_attr, textalt* } diff -r a5265222d6e6 -r 972c4f42fd52 lib/ProofGeneral/schemas.xml --- a/lib/ProofGeneral/schemas.xml Sat May 11 16:00:24 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,5 +0,0 @@ - - - - - diff -r a5265222d6e6 -r 972c4f42fd52 lib/Tools/mkproject --- a/lib/Tools/mkproject Sat May 11 16:00:24 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,25 +0,0 @@ -#!/usr/bin/env bash -# -# Author: David Aspinall -# -# DESCRIPTION: prepare a session directory for PG-Eclipse - -PRG="$(basename "$0")" - -function usage() -{ - echo - echo "Usage: isabelle $PRG NAME" - echo - echo " Prepare a session directory for PG-Eclipse." - exit 1 -} - -if [ "$#" -eq 1 ]; then - NAME="$1"; shift -else - usage -fi - -"$ISABELLE_TOOL" mkdir -b -q "$NAME" -( cd document; "$ISABELLE_TOOL" latex -o sty; ) diff -r a5265222d6e6 -r 972c4f42fd52 src/Doc/System/Basics.thy --- a/src/Doc/System/Basics.thy Sat May 11 16:00:24 2013 +0200 +++ b/src/Doc/System/Basics.thy Sat May 11 22:20:59 2013 +0200 @@ -383,7 +383,6 @@ -S secure mode -- disallow critical operations -T ADDR startup process wrapper, with socket address -W IN:OUT startup process wrapper, with input/output fifos - -X startup PGIP interaction mode -e MLTEXT pass MLTEXT to the ML session -f pass 'Session.finish();' to the ML session -m MODE add print mode for output @@ -456,8 +455,7 @@ \medskip The @{verbatim "-I"} option makes Isabelle enter Isar interaction mode on startup, instead of the primitive ML top-level. The @{verbatim "-P"} option configures the top-level loop for - interaction with the Proof General user interface, and the - @{verbatim "-X"} option enables XML-based PGIP communication. + interaction with the Proof General user interface. \medskip The @{verbatim "-T"} or @{verbatim "-W"} option makes Isabelle enter a special process wrapper for interaction via diff -r a5265222d6e6 -r 972c4f42fd52 src/HOL/BNF/Tools/bnf_def.ML --- a/src/HOL/BNF/Tools/bnf_def.ML Sat May 11 16:00:24 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_def.ML Sat May 11 22:20:59 2013 +0200 @@ -123,7 +123,7 @@ {map_id = id, map_comp = comp, map_cong0 = cong, set_map = nat, bd_card_order = c_o, bd_cinfinite = cinf, set_bd = set_bd, in_bd = in_bd, map_wpull = wpull, rel_OO_Grp = rel}; -fun dest_cons [] = raise Empty +fun dest_cons [] = raise List.Empty | dest_cons (x :: xs) = (x, xs); fun mk_axioms n thms = thms diff -r a5265222d6e6 -r 972c4f42fd52 src/HOL/Library/Debug.thy --- a/src/HOL/Library/Debug.thy Sat May 11 16:00:24 2013 +0200 +++ b/src/HOL/Library/Debug.thy Sat May 11 22:20:59 2013 +0200 @@ -30,6 +30,7 @@ [simp]: "timing s f x = f x" code_const trace and flush and timing + (* FIXME proper @{make_string} instead of PolyML.makestring?!?! *) (Eval "Output.tracing" and "Output.tracing/ (PolyML.makestring _)" and "Timing.timeap'_msg") code_reserved Eval Output PolyML Timing diff -r a5265222d6e6 -r 972c4f42fd52 src/HOL/Matrix_LP/Cplex_tools.ML --- a/src/HOL/Matrix_LP/Cplex_tools.ML Sat May 11 16:00:24 2013 +0200 +++ b/src/HOL/Matrix_LP/Cplex_tools.ML Sat May 11 22:20:59 2013 +0200 @@ -973,7 +973,7 @@ result end handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s)) - | Option => raise (Load_cplexResult "Option") + | Option.Option => raise (Load_cplexResult "Option") fun load_cplexResult name = let @@ -1122,7 +1122,7 @@ result end handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s)) - | Option => raise (Load_cplexResult "Option") + | Option.Option => raise (Load_cplexResult "Option") exception Execute of string; diff -r a5265222d6e6 -r 972c4f42fd52 src/HOL/Metis_Examples/Type_Encodings.thy --- a/src/HOL/Metis_Examples/Type_Encodings.thy Sat May 11 16:00:24 2013 +0200 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy Sat May 11 22:20:59 2013 +0200 @@ -56,7 +56,7 @@ let fun tac [] st = all_tac st | tac (type_enc :: type_encs) st = - st (* |> tap (fn _ => tracing (PolyML.makestring type_enc)) *) + st (* |> tap (fn _ => tracing (@{make_string} type_enc)) *) |> ((if null type_encs then all_tac else rtac @{thm fork} 1) THEN Metis_Tactic.metis_tac [type_enc] ATP_Problem_Generate.combsN ctxt ths 1 diff -r a5265222d6e6 -r 972c4f42fd52 src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Sat May 11 16:00:24 2013 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Sat May 11 22:20:59 2013 +0200 @@ -722,12 +722,12 @@ (* for debugging only: fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) = "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^ - "; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^ + "; tysubst: " ^ @{make_string} tysubst ^ "; tsubst: {" ^ commas (map ((fn (s, t) => s ^ " |-> " ^ t) o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}" - val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters) - val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts) - val _ = tracing ("OUTER PARAMS: " ^ PolyML.makestring outer_param_names) + val _ = tracing ("ORDERED CLUSTERS: " ^ @{make_string} ordered_clusters) + val _ = tracing ("AXIOM COUNTS: " ^ @{make_string} ax_counts) + val _ = tracing ("OUTER PARAMS: " ^ @{make_string} outer_param_names) val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^ cat_lines (map string_for_subst_info substs)) *) diff -r a5265222d6e6 -r 972c4f42fd52 src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Sat May 11 16:00:24 2013 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Sat May 11 22:20:59 2013 +0200 @@ -194,7 +194,7 @@ [s] => the_default (s, s) (first_field "\" s) | ["", s2] => ("-" ^ s2, "-" ^ s2) | [s1, s2] => (s1, s2) - | _ => raise Option) + | _ => raise Option.Option) |> pairself (maxed_int_from_string min_int) in if k1 <= k2 then k1 upto k2 else k1 downto k2 end handle Option.Option => diff -r a5265222d6e6 -r 972c4f42fd52 src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Sat May 11 16:00:24 2013 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Sat May 11 22:20:59 2013 +0200 @@ -384,9 +384,9 @@ (ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty in fn ct => the (Inttab.lookup tab (ct |> term_of |> dest_number)) - handle Option => + handle Option.Option => (writeln ("noz: Theorems-Table contains no entry for " ^ - Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option) + Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option.Option) end fun unit_conv t = case (term_of t) of @@ -472,9 +472,9 @@ val dvd = let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in fn ct => the (Inttab.lookup tab (term_of ct |> dest_number)) - handle Option => + handle Option.Option => (writeln ("dvd: Theorems-Table contains no entry for" ^ - Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option) + Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option.Option) end val dp = let val th = Simplifier.rewrite (put_simpset lin_ss ctxt) @@ -541,9 +541,9 @@ sths) Termtab.empty in fn ct => the (Termtab.lookup tab (term_of ct)) - handle Option => + handle Option.Option => (writeln ("inS: No theorem for " ^ Syntax.string_of_term ctxt (Thm.term_of ct)); - raise Option) + raise Option.Option) end val (inf, nb, pd) = divide_and_conquer (f x dvd inS (abths S)) p in [dp, inf, nb, pd] MRS cpth diff -r a5265222d6e6 -r 972c4f42fd52 src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Sat May 11 16:00:24 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Sat May 11 22:20:59 2013 +0200 @@ -41,9 +41,9 @@ fun pop tab key = (let val v = hd (Inttab.lookup_list tab key) in (v, Inttab.remove_list (op =) (key, v) tab) - end) handle Empty => raise Fail "sledgehammer_compress: pop" + end) handle List.Empty => raise Fail "sledgehammer_compress: pop" fun pop_max tab = pop tab (the (Inttab.max_key tab)) - handle Option => raise Fail "sledgehammer_compress: pop_max" + handle Option.Option => raise Fail "sledgehammer_compress: pop_max" fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab (* Main function for compresing proofs *) @@ -55,8 +55,7 @@ (* handle metis preplay fail *) local - open Unsynchronized - val metis_fail = ref false + val metis_fail = Unsynchronized.ref false in fun handle_metis_fail try_metis () = try_metis () handle exn => @@ -104,7 +103,7 @@ | (Prove (_, _, t, By_Metis _), Obtain (_, _, _, _, By_Metis _)) => cons (Term.size_of_term t, i) | _ => I) - handle Option => raise Fail "sledgehammer_compress: add_if_cand") + handle Option.Option => raise Fail "sledgehammer_compress: add_if_cand") | add_if_cand _ _ = I val cand_tab = v_fold_index (add_if_cand step_vect) refed_by_vect [] @@ -121,7 +120,7 @@ #> handle_metis_fail #> Lazy.lazy) step_vect - handle Option => raise Fail "sledgehammer_compress: metis_time" + handle Option.Option => raise Fail "sledgehammer_compress: metis_time" fun sum_up_time lazy_time_vector = Vector.foldl @@ -204,7 +203,7 @@ (n_metis' - 1) end end - handle Option => raise Fail "sledgehammer_compress: merge_steps" + handle Option.Option => raise Fail "sledgehammer_compress: merge_steps" | List.Empty => raise Fail "sledgehammer_compress: merge_steps" in merge_steps metis_time step_vect refed_by_vect cand_tab n n_metis diff -r a5265222d6e6 -r 972c4f42fd52 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sat May 11 16:00:24 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sat May 11 22:20:59 2013 +0200 @@ -58,11 +58,11 @@ fun parse_bool_option option name s = (case s of - "smart" => if option then NONE else raise Option + "smart" => if option then NONE else raise Option.Option | "false" => SOME false | "true" => SOME true | "" => SOME true - | _ => raise Option) + | _ => raise Option.Option) handle Option.Option => let val ss = map quote ((option ? cons "smart") ["true", "false"]) in error ("Parameter " ^ quote name ^ " must be assigned " ^ diff -r a5265222d6e6 -r 972c4f42fd52 src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Sat May 11 16:00:24 2013 +0200 +++ b/src/HOL/Tools/TFL/tfl.ML Sat May 11 22:20:59 2013 +0200 @@ -604,7 +604,7 @@ val vlist = #2 (USyntax.strip_comb (USyntax.rhs body)) val plist = ListPair.zip (vlist, xlist) val args = map (the o AList.lookup (op aconv) plist) qvars - handle Option => raise Fail "TFL.alpha_ex_unroll: no correspondence" + handle Option.Option => raise Fail "TFL.alpha_ex_unroll: no correspondence" fun build ex [] = [] | build (_$rex) (v::rst) = let val ex1 = Term.betapply(rex, v) diff -r a5265222d6e6 -r 972c4f42fd52 src/HOL/Tools/groebner.ML --- a/src/HOL/Tools/groebner.ML Sat May 11 16:00:24 2013 +0200 +++ b/src/HOL/Tools/groebner.ML Sat May 11 22:20:59 2013 +0200 @@ -864,7 +864,7 @@ val (vars,bod) = strip_exists tm val cjs = striplist (dest_binary @{cterm HOL.conj}) bod val th1 = (the (get_first (try (isolate_variable vars)) cjs) - handle Option => raise CTERM ("unwind_polys_conv",[tm])) + handle Option.Option => raise CTERM ("unwind_polys_conv",[tm])) val eq = Thm.lhs_of th1 val bod' = list_mk_binop @{cterm HOL.conj} (eq::(remove op aconvc eq cjs)) val th2 = conj_ac_rule (mk_eq bod bod') diff -r a5265222d6e6 -r 972c4f42fd52 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Sat May 11 16:00:24 2013 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Sat May 11 22:20:59 2013 +0200 @@ -498,7 +498,7 @@ (case try_add ([thm1] RL inj_thms) thm2 of NONE => (the (try_add ([thm2] RL inj_thms) thm1) - handle Option => + handle Option.Option => (trace_thm ctxt [] thm1; trace_thm ctxt [] thm2; raise Fail "Linear arithmetic: failed to add thms")) | SOME thm => thm) diff -r a5265222d6e6 -r 972c4f42fd52 src/Pure/General/basics.ML --- a/src/Pure/General/basics.ML Sat May 11 16:00:24 2013 +0200 +++ b/src/Pure/General/basics.ML Sat May 11 22:20:59 2013 +0200 @@ -78,7 +78,7 @@ | is_none NONE = true; fun the (SOME x) = x - | the NONE = raise Option; + | the NONE = raise Option.Option; fun these (SOME x) = x | these NONE = []; diff -r a5265222d6e6 -r 972c4f42fd52 src/Pure/ProofGeneral/TODO --- a/src/Pure/ProofGeneral/TODO Sat May 11 16:00:24 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -Major: - - Complete pgip_types: add PGML and objtypes - Complete pgip_markup: provide markup abstraction for parsing.ML - -Minor: - - cleanups: signatures & structures, concrete types in XML attrs, etc. - further tests in pgip_tests.ML diff -r a5265222d6e6 -r 972c4f42fd52 src/Pure/ProofGeneral/pgip.ML --- a/src/Pure/ProofGeneral/pgip.ML Sat May 11 16:00:24 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,22 +0,0 @@ -(* Title: Pure/ProofGeneral/pgip.ML - Author: David Aspinall - -Prover-side PGIP abstraction. -Not too closely tied to Isabelle, to help with reuse/porting. -*) - -signature PGIP = -sig - include PGIPTYPES - include PGIPMARKUP - include PGIPINPUT - include PGIPOUTPUT -end - -structure Pgip : PGIP = -struct - open PgipTypes - open PgipMarkup - open PgipInput - open PgipOutput -end diff -r a5265222d6e6 -r 972c4f42fd52 src/Pure/ProofGeneral/pgip_tests.ML --- a/src/Pure/ProofGeneral/pgip_tests.ML Sat May 11 16:00:24 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,129 +0,0 @@ -(* Title: Pure/ProofGeneral/pgip_tests.ML - Author: David Aspinall - -A test suite for the PGIP abstraction code (in progress). -Run to provide some mild insurance against breakage in Isabelle here. -*) - -(** pgip_types.ML **) - -local -fun asseq_p toS a b = - if a=b then () - else error("PGIP test: expected these two values to be equal:\n" ^ - (toS a) ^"\n and: \n" ^ (toS b)) - -val asseqx = asseq_p XML.string_of -val asseqs = asseq_p I -val asseqb = asseq_p (fn b=>if b then "true" else "false") - -open PgipTypes; -in - -val _ = asseqx (pgiptype_to_xml Pgipnull) (XML.parse ""); -val _ = asseqx (pgiptype_to_xml Pgipbool) (XML.parse ""); -val _ = asseqx (pgiptype_to_xml (Pgipint (NONE,NONE))) (XML.parse ""); -val _ = asseqx (pgiptype_to_xml (Pgipint (SOME 5,SOME 7))) (XML.parse ""); -val _ = asseqx (pgiptype_to_xml (Pgipint (NONE,SOME 7))) (XML.parse ""); -val _ = asseqx (pgiptype_to_xml (Pgipint (SOME ~5,NONE))) (XML.parse ""); -val _ = asseqx (pgiptype_to_xml Pgipstring) (XML.parse ""); -val _ = asseqx (pgiptype_to_xml (Pgipconst "radio1")) (XML.parse ""); -val _ = asseqx (pgiptype_to_xml (Pgipchoice [Pgipdtype (SOME "the best choice",Pgipbool)])) - (XML.parse ""); - -val _ = asseqs (pgval_to_string (read_pgval Pgipbool "true")) "true"; -val _ = asseqs (pgval_to_string (read_pgval Pgipbool "false")) "false"; -val _ = asseqs (pgval_to_string (read_pgval (Pgipint(NONE,NONE)) "-37")) "-37"; -val _ = asseqs (pgval_to_string (read_pgval Pgipnat "45")) "45"; -val _ = asseqs (pgval_to_string (read_pgval Pgipstring "stringvalue")) "stringvalue"; - -local - val choices = Pgipchoice [Pgipdtype (NONE,Pgipbool), Pgipdtype (NONE,Pgipnat), - Pgipdtype (NONE,Pgipnull), Pgipdtype (NONE,Pgipconst "foo")] -in -val _ = asseqs (pgval_to_string (read_pgval choices "45")) "45"; -val _ = asseqs (pgval_to_string (read_pgval choices "foo")) "foo"; -val _ = asseqs (pgval_to_string (read_pgval choices "true")) "true"; -val _ = asseqs (pgval_to_string (read_pgval choices "")) ""; -val _ = (asseqs (pgval_to_string (read_pgval choices "-37")) "-37"; - error "pgip_tests: should fail") handle PGIP _ => () -end - -val _ = asseqx (haspref {name="provewithgusto",descr=SOME "use energetic proofs", - default=SOME "true", pgiptype=Pgipbool}) - (XML.parse ""); -end - - -(** pgip_input.ML **) -local - -fun e str = case XML.parse str of - (XML.Elem args) => args - | _ => error("Expected to get an XML Element") - -open PgipInput; -open PgipTypes; -open PgipIsabelle; - -fun asseqi a b = - if input (e a) = b then () - else error("PGIP test: expected two inputs to be equal, for input:\n" ^ a) - -in - -val _ = asseqi "" (SOME (Askpgip())); -val _ = asseqi "" (SOME (Askpgml())); -val _ = asseqi "" (SOME (Askconfig())); -(* FIXME: new tests: -val _ = asseqi "" (SOME (Pgmlsymbolson())); -val _ = asseqi "" (SOME (Pgmlsymbolsoff())); -val _ = asseqi "" (SOME (Startquiet())); -val _ = asseqi "" (SOME (Stopquiet())); -*) -val _ = asseqi "" (SOME (Askrefs {url=NONE, thyname=SOME "foo", - objtype=SOME ObjTheory,name=NONE})); -val _ = asseqi "" NONE; - -end - -(** pgip_markup.ML **) -local -open PgipMarkup -in -val _ = () -end - - -(** pgip_output.ML **) -local -open PgipOutput -in -val _ = () -end - - -(** pgip_parser.ML **) -local -open PgipMarkup -open PgipParser -open PgipIsabelle - -fun asseqp a b = - if pgip_parser Position.none a = b then () - else error("PGIP test: expected two parses to be equal, for input:\n" ^ a) - -in -val _ = - asseqp "theory A imports Bthy Cthy Dthy begin" - [Opentheory - {text = "theory A imports Bthy Cthy Dthy begin", - thyname = SOME "A", - parentnames = ["Bthy", "Cthy", "Dthy"]}, - Openblock {metavarid=NONE,name=NONE,objtype=SOME ObjTheoryBody}]; - -val _ = - asseqp "end" - [Closeblock {}, Closetheory {text = "end"}]; - -end diff -r a5265222d6e6 -r 972c4f42fd52 src/Pure/ProofGeneral/proof_general_emacs.ML --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Sat May 11 16:00:24 2013 +0200 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Sat May 11 22:20:59 2013 +0200 @@ -236,7 +236,7 @@ Output.default_output Output.default_escape; Markup.add_mode ProofGeneralPgip.proof_general_emacsN YXML.output_markup; setup_messages (); - ProofGeneralPgip.pgip_channel_emacs (! Output.Private_Hooks.urgent_message_fn); + ProofGeneralPgip.init_pgip_session_id (); setup_thy_loader (); setup_present_hook (); initialized := true); diff -r a5265222d6e6 -r 972c4f42fd52 src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Sat May 11 16:00:24 2013 +0200 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Sat May 11 22:20:59 2013 +0200 @@ -12,7 +12,7 @@ val new_thms_deps: theory -> theory -> string list * string list val init_pgip: bool -> unit (* main PGIP loop with true; fail with false *) - val pgip_channel_emacs: (string -> unit) -> unit + val init_pgip_session_id: unit -> unit (* More message functions... *) val nonfatal_error : string -> unit (* recoverable (batch) error: carry on scripting *) @@ -26,7 +26,10 @@ structure ProofGeneralPgip : PROOF_GENERAL_PGIP = struct -open Pgip; +open PgipTypes; +open PgipMarkup; +open PgipInput; +open PgipOutput; (** print mode **) @@ -251,7 +254,7 @@ thms |> fold (fn (_, (name, _, _)) => name <> "" ? Symtab.update (name, ())); fun add_thm th = - (case Thm.proof_body_of th of + (case Thm.proof_body_of th of PBody {proof = PThm (_, ((name, _, _), body)), ...} => if Thm.has_name_hint th andalso Thm.get_name_hint th = name then add_proof_body (Future.join body) @@ -368,6 +371,11 @@ fun add_preference cat pref = CRITICAL (fn () => Unsynchronized.change preferences (Preferences.add cat pref)); +fun set_preference pref value = + (case AList.lookup (op =) (map (fn p => (#name p, p)) (maps snd (! preferences))) pref of + SOME {set, ...} => set value + | NONE => error ("Unknown prover preference: " ^ quote pref)); + fun setup_preferences_tweak () = CRITICAL (fn () => Unsynchronized.change preferences (Preferences.set_default ("show-question-marks", "false") #> @@ -845,50 +853,50 @@ fun quitpgip _ = raise PGIP_QUIT fun process_input inp = case inp - of Pgip.Askpgip _ => askpgip inp - | Pgip.Askpgml _ => askpgml inp - | Pgip.Askprefs _ => askprefs inp - | Pgip.Askconfig _ => askconfig inp - | Pgip.Getpref _ => getpref inp - | Pgip.Setpref _ => setpref inp - | Pgip.Proverinit _ => proverinit inp - | Pgip.Proverexit _ => proverexit inp - | Pgip.Setproverflag _ => setproverflag inp - | Pgip.Dostep _ => dostep inp - | Pgip.Undostep _ => undostep inp - | Pgip.Redostep _ => redostep inp - | Pgip.Forget _ => error " not implemented by Isabelle" - | Pgip.Restoregoal _ => error " not implemented by Isabelle" - | Pgip.Abortgoal _ => abortgoal inp - | Pgip.Askids _ => askids inp - | Pgip.Askrefs _ => askrefs inp - | Pgip.Showid _ => showid inp - | Pgip.Askguise _ => askguise inp - | Pgip.Parsescript _ => parsescript inp - | Pgip.Showproofstate _ => showproofstate inp - | Pgip.Showctxt _ => showctxt inp - | Pgip.Searchtheorems _ => searchtheorems inp - | Pgip.Setlinewidth _ => setlinewidth inp - | Pgip.Viewdoc _ => viewdoc inp - | Pgip.Doitem _ => doitem inp - | Pgip.Undoitem _ => undoitem inp - | Pgip.Redoitem _ => redoitem inp - | Pgip.Aborttheory _ => aborttheory inp - | Pgip.Retracttheory _ => retracttheory inp - | Pgip.Loadfile _ => loadfile inp - | Pgip.Openfile _ => openfile inp - | Pgip.Closefile _ => closefile inp - | Pgip.Abortfile _ => abortfile inp - | Pgip.Retractfile _ => retractfile inp - | Pgip.Changecwd _ => changecwd inp - | Pgip.Systemcmd _ => systemcmd inp - | Pgip.Quitpgip _ => quitpgip inp + of PgipInput.Askpgip _ => askpgip inp + | PgipInput.Askpgml _ => askpgml inp + | PgipInput.Askprefs _ => askprefs inp + | PgipInput.Askconfig _ => askconfig inp + | PgipInput.Getpref _ => getpref inp + | PgipInput.Setpref _ => setpref inp + | PgipInput.Proverinit _ => proverinit inp + | PgipInput.Proverexit _ => proverexit inp + | PgipInput.Setproverflag _ => setproverflag inp + | PgipInput.Dostep _ => dostep inp + | PgipInput.Undostep _ => undostep inp + | PgipInput.Redostep _ => redostep inp + | PgipInput.Forget _ => error " not implemented by Isabelle" + | PgipInput.Restoregoal _ => error " not implemented by Isabelle" + | PgipInput.Abortgoal _ => abortgoal inp + | PgipInput.Askids _ => askids inp + | PgipInput.Askrefs _ => askrefs inp + | PgipInput.Showid _ => showid inp + | PgipInput.Askguise _ => askguise inp + | PgipInput.Parsescript _ => parsescript inp + | PgipInput.Showproofstate _ => showproofstate inp + | PgipInput.Showctxt _ => showctxt inp + | PgipInput.Searchtheorems _ => searchtheorems inp + | PgipInput.Setlinewidth _ => setlinewidth inp + | PgipInput.Viewdoc _ => viewdoc inp + | PgipInput.Doitem _ => doitem inp + | PgipInput.Undoitem _ => undoitem inp + | PgipInput.Redoitem _ => redoitem inp + | PgipInput.Aborttheory _ => aborttheory inp + | PgipInput.Retracttheory _ => retracttheory inp + | PgipInput.Loadfile _ => loadfile inp + | PgipInput.Openfile _ => openfile inp + | PgipInput.Closefile _ => closefile inp + | PgipInput.Abortfile _ => abortfile inp + | PgipInput.Retractfile _ => retractfile inp + | PgipInput.Changecwd _ => changecwd inp + | PgipInput.Systemcmd _ => systemcmd inp + | PgipInput.Quitpgip _ => quitpgip inp fun process_pgip_element pgipxml = case pgipxml of xml as (XML.Elem elem) => - (case Pgip.input elem of + (case PgipInput.input elem of NONE => warning ("Unrecognized PGIP command, ignored: \n" ^ (XML.string_of xml)) | SOME inp => (process_input inp)) (* errors later; packet discarded *) @@ -1009,32 +1017,65 @@ (** Out-of-loop PGIP commands (for Emacs hybrid mode) **) local - val pgip_output_channel = Unsynchronized.ref Output.physical_writeln + +fun invalid_pgip () = raise PGIP "Invalid PGIP packet received"; + +fun output_emacs pgips = Output.urgent_message (output_pgips pgips); + +fun process_element_emacs (XML.Elem (("askprefs", _), _)) = + let + fun preference_of {name, descr, default, pgiptype, get, set} = + {name = name, descr = SOME descr, default = SOME default, pgiptype = pgiptype}; + in + ! preferences |> List.app (fn (prefcat, prefs) => + output_emacs [Hasprefs {prefcategory = SOME prefcat, prefs = map preference_of prefs}]) + end + | process_element_emacs (XML.Elem (("setpref", attrs), data)) = + let + val name = + (case Properties.get attrs "name" of + SOME name => name + | NONE => invalid_pgip ()); + val value = XML.content_of data; + in set_preference name value end + | process_element_emacs _ = invalid_pgip (); + in -(* Set recipient for PGIP results *) -fun pgip_channel_emacs writefn = - (init_pgip_session_id(); - pgip_output_channel := writefn) - -(* Process a PGIP command. - This works for preferences but not generally guaranteed - because we haven't done full setup here (e.g., no pgml mode) *) fun process_pgip_emacs str = - Unsynchronized.setmp output_xml_fn (!pgip_output_channel) process_pgip_plain str - -end - - -(* Extra command for embedding prover-control inside document (obscure/debug usage). *) + let + val _ = pgip_refid := NONE; + val _ = pgip_refseq := NONE; + in + (case XML.parse str of + XML.Elem (("pgip", attrs), pgips) => + let + val class = PgipTypes.get_attr "class" attrs; + val dest = PgipTypes.get_attr_opt "destid" attrs; + val seq = PgipTypes.read_pgipnat (PgipTypes.get_attr "seq" attrs); + val processit = + (case dest of + NONE => class = "pa" + | SOME id => matching_pgip_id id); + in + if processit then + (pgip_refid := PgipTypes.get_attr_opt "id" attrs; + pgip_refseq := SOME seq; + List.app process_element_emacs pgips) + else () + end + | _ => invalid_pgip ()) + end handle PGIP msg => error (msg ^ "\n" ^ str); val _ = Outer_Syntax.improper_command (("ProofGeneral.process_pgip", Keyword.control), Position.none) "(internal)" (Parse.text >> - (fn txt => Toplevel.imperative (fn () => + (fn str => Toplevel.imperative (fn () => if print_mode_active proof_general_emacsN - then process_pgip_emacs txt - else process_pgip_plain txt))); + then process_pgip_emacs str + else process_pgip_plain str))); end; + +end; diff -r a5265222d6e6 -r 972c4f42fd52 src/Pure/ROOT --- a/src/Pure/ROOT Sat May 11 16:00:24 2013 +0200 +++ b/src/Pure/ROOT Sat May 11 22:20:59 2013 +0200 @@ -160,13 +160,11 @@ "Proof/proof_rewrite_rules.ML" "Proof/proof_syntax.ML" "Proof/reconstruct.ML" - "ProofGeneral/pgip.ML" "ProofGeneral/pgip_input.ML" "ProofGeneral/pgip_isabelle.ML" "ProofGeneral/pgip_markup.ML" "ProofGeneral/pgip_output.ML" "ProofGeneral/pgip_parser.ML" - "ProofGeneral/pgip_tests.ML" "ProofGeneral/pgip_types.ML" "ProofGeneral/pgml.ML" "ProofGeneral/preferences.ML" diff -r a5265222d6e6 -r 972c4f42fd52 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Sat May 11 16:00:24 2013 +0200 +++ b/src/Pure/ROOT.ML Sat May 11 22:20:59 2013 +0200 @@ -302,7 +302,6 @@ use "ProofGeneral/pgip_markup.ML"; use "ProofGeneral/pgip_input.ML"; use "ProofGeneral/pgip_output.ML"; -use "ProofGeneral/pgip.ML"; use "ProofGeneral/pgip_isabelle.ML"; @@ -348,8 +347,6 @@ toplevel_pp ["typ"] "Proof_Display.pp_typ Pure.thy"; -use "ProofGeneral/pgip_tests.ML"; - (* ML toplevel commands *) diff -r a5265222d6e6 -r 972c4f42fd52 src/Pure/type.ML --- a/src/Pure/type.ML Sat May 11 16:00:24 2013 +0200 +++ b/src/Pure/type.ML Sat May 11 22:20:59 2013 +0200 @@ -379,11 +379,11 @@ fun freeze_one alist (ix, sort) = TFree (the (AList.lookup (op =) alist ix), sort) - handle Option => + handle Option.Option => raise TYPE ("Failure during freezing of ?" ^ string_of_indexname ix, [], []); fun thaw_one alist (a, sort) = TVar (the (AList.lookup (op =) alist a), sort) - handle Option => TFree (a, sort); + handle Option.Option => TFree (a, sort); in diff -r a5265222d6e6 -r 972c4f42fd52 src/Tools/Code/code_namespace.ML --- a/src/Tools/Code/code_namespace.ML Sat May 11 16:00:24 2013 +0200 +++ b/src/Tools/Code/code_namespace.ML Sat May 11 22:20:59 2013 +0200 @@ -125,7 +125,7 @@ Long_Name.append (fst (dest_name name)) (base_deresolver name) | deresolver module_name name = the (Symtab.lookup (the (Symtab.lookup deresolver_tab module_name)) name) - handle Option => error ("Unknown statement name: " ^ labelled_name name); + handle Option.Option => error ("Unknown statement name: " ^ labelled_name name); in { deresolver = deresolver, flat_program = flat_program } end; diff -r a5265222d6e6 -r 972c4f42fd52 src/Tools/WWW_Find/http_util.ML --- a/src/Tools/WWW_Find/http_util.ML Sat May 11 16:00:24 2013 +0200 +++ b/src/Tools/WWW_Find/http_util.ML Sat May 11 22:20:59 2013 +0200 @@ -46,7 +46,7 @@ |> Char.chr |> String.str |> Substring.full - handle Option => c; + handle Option.Option => c; fun f (done, s) = let diff -r a5265222d6e6 -r 972c4f42fd52 src/Tools/WWW_Find/socket_util.ML --- a/src/Tools/WWW_Find/socket_util.ML Sat May 11 16:00:24 2013 +0200 +++ b/src/Tools/WWW_Find/socket_util.ML Sat May 11 22:20:59 2013 +0200 @@ -26,7 +26,7 @@ |> NetHostDB.addr |> rpair port |> INetSock.toAddr - handle Option => raise Fail ("Cannot resolve hostname: " ^ host)); + handle Option.Option => raise Fail ("Cannot resolve hostname: " ^ host)); val _ = Socket.bind (sock, addr); val _ = Socket.listen (sock, 5); in sock end; diff -r a5265222d6e6 -r 972c4f42fd52 src/ZF/Datatype_ZF.thy --- a/src/ZF/Datatype_ZF.thy Sat May 11 16:00:24 2013 +0200 +++ b/src/ZF/Datatype_ZF.thy Sat May 11 22:20:59 2013 +0200 @@ -81,9 +81,9 @@ val lname = #1 (dest_Const lhead) handle TERM _ => raise Match; val rname = #1 (dest_Const rhead) handle TERM _ => raise Match; val lcon_info = the (Symtab.lookup (ConstructorsData.get thy) lname) - handle Option => raise Match; + handle Option.Option => raise Match; val rcon_info = the (Symtab.lookup (ConstructorsData.get thy) rname) - handle Option => raise Match; + handle Option.Option => raise Match; val new = if #big_rec_name lcon_info = #big_rec_name rcon_info andalso not (null (#free_iffs lcon_info)) then diff -r a5265222d6e6 -r 972c4f42fd52 src/ZF/Tools/primrec_package.ML --- a/src/ZF/Tools/primrec_package.ML Sat May 11 16:00:24 2013 +0200 +++ b/src/ZF/Tools/primrec_package.ML Sat May 11 22:20:59 2013 +0200 @@ -49,7 +49,7 @@ val (cname, _) = dest_Const constr handle TERM _ => raise RecError "ill-formed constructor"; val con_info = the (Symtab.lookup (ConstructorsData.get thy) cname) - handle Option => + handle Option.Option => raise RecError "cannot determine datatype associated with function" val (ls, cargs, rs) = (map dest_Free ls_frees,