--- 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
--- 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.
-
--- 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 = <any non-empty character sequence>
-# 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 <parsescript> 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 <ready/>, 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 <parsescript> to
-# generate error messages for particular locations; they can be used
-# in <parseresult> 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'.
-
--- 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 @@
-<!-- Title: Pure/pgip_isar.xml
- Author: David Aspinall, University of Edinburgh
- Author: Christoph Lüth, University of Bremen
-
-This file contains the configuration messages which configure
-PGIP interfaces for Isabelle/Isar, in particular, explaining
-internal types of objects and operations available on them.
-
-See http://proofgeneral.inf.ed.ac.uk/kit for more details.
-
-This file is a contributed part of the Isabelle Distribution.
-
-STATUS: incomplete and experimental.
--->
-
-<displayconfig>
-
- <welcomemsg>Welcome to Isabelle/Isar 2007.</welcomemsg>
-
- <!-- Icon for Isabelle interface -->
- <icon>
- 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==
- </icon>
-
- <helpdoc name="Isabelle/HOL Tutorial"
- descr="A gentle introduction to Isabelle/HOL"
- url="http://isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf"
- >tutorial</helpdoc>
- <helpdoc name="Isabelle HOL Logic Reference"
- descr="The Isabelle HOL Logic in detail"
- url="http://isabelle.in.tum.de/dist/Isabelle/doc/logics-HOL.pdf"
- >logics-HOL</helpdoc>
- <helpdoc name="Isar Tutorial"
- descr="An Introduction to the Isar proof language"
- url="http://isabelle.in.tum.de/dist/Isabelle/doc/isar-overview.pdf"
- >isar-overview</helpdoc>
- <helpdoc name="Isabelle/Isar Reference"
- descr="Reference Manual for Isabelle/Isar"
- url="http://isabelle.in.tum.de/dist/Isabelle/doc/isar-ref.pdf"
- >isar-ref</helpdoc>
- <helpdoc name="Isabelle Reference manual"
- descr="Reference Manual for Isabelle"
- url="http://isabelle.in.tum.de/dist/Isabelle/doc/ref.pdf"
- >ref</helpdoc>
- <helpdoc
- name="Isabelle System manual"
- descr="System Manual: interfaces, output, building logics."
- url="http://isabelle.in.tum.de/dist/Isabelle/doc/system.pdf"
- >system</helpdoc>
-
- <!-- Example lexicalstructure element. This is incomplete and the
- keywords need to be filled dynamically -->
- <lexicalstructure>
- <keyword word="begin"><shorthelp>Begin theory or proof</shorthelp></keyword>
- <keyword word="end"><shorthelp>End theory or proof</shorthelp></keyword>
- <stringdelimiter>"</stringdelimiter>
- <commentdelimiter start="(*" end="*)"/>
- <commentdelimiter start="--"/>
- <identifiersyntax initialchars="abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"
- allowedchars="abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ012345689_'"/>
- </lexicalstructure>
-
-
- <!-- objtypes -->
-
- <objtype name="toplevel" descr="top-level context (PGIP internal)">
- <contains objtype="theory"/>
- </objtype>
-
- <objtype name="theory" descr="Isabelle theory">
- <contains objtype="theorem"/>
- <contains objtype="theory"/>
- </objtype>
-
- <objtype name="theorem" descr="Isabelle theorem">
- <contains objtype="theorem-proof"/>
- <hasprefs prefcategory="Theorem attributes">
- <haspref name="thm-kind" descr="Theorem kind">
- <pgipchoice>
- <pgipconst name="theorem" descr="Theorem"/>
- <pgipconst name="lemma" descr="Lemma"/>
- <pgipconst name="corollary" descr="Corollary"/>
- </pgipchoice>
- </haspref>
- <haspref name="thm-simp" descr="Include in simplifier set">
- <pgipbool/>
- </haspref>
- <haspref name="thm-intro" descr="Flag as introduction rule">
- <pgipbool/>
- </haspref>
- <haspref name="thm-elim" descr="Flag as elimination rule">
- <pgipbool/>
- </haspref>
- <haspref name="thm-dest" descr="Flag as destruction rule">
- <pgipbool/>
- </haspref>
- </hasprefs>
- </objtype>
- <objtype name="theorem-proof" descr="Isabelle proof">
- </objtype>
- <objtype name="term" descr="Isabelle term">
- <icon>
- R0lGODlhJgAgAIQAAP////r6+uDg4Nra2tnZ2fn5+WFhYUJCQkFBQWBgYMnO
- 91xq6K208wsg3XiD7OTm+0FR5CY54Pb29t3d3dfX119fX/T09NbW1tjY2AAA
- AAAAAAAAAAAAAAAAAAAAAAAAACH+FUNyZWF0ZWQgd2l0aCBUaGUgR0lNUAAh
- +QQBCgAfACwAAAAAJgAgAAAFnCAgjmRpnqgYCAPhvnAsz7BQAIJxIHzv/8Cg
- LyHA6YTI5I8IWLVo0Gjtlqpar9istqRYLBTbMIDRaDDEW7IZrVWf2VYGw1F2
- yBkP+KnM77/1Jm6AcWV/gyeChyiJioGFjYiPkCWMkyKVlpiTmpBqEJYlEWUR
- XgugDBCjDnmgrZMSExQUUrQ0NgADFUq7SUy5vMBATBYDFxi1yFMAIQA7
- </icon>
- </objtype>
- <objtype name="type" descr="Isabelle type">
- <icon>
- R0lGODlhJgAgAIQAAP////r6+uDg4Nra2tnZ2fn5+WFhYUJCQkFBQWBgYOTm
- +62080FR5Asg3SY54Fxq6MnO95Kc73iD7Pb29t3d3dfX119fX/T09NbW1tjY
- 2AAAAAAAAAAAAAAAAAAAAAAAACH+FUNyZWF0ZWQgd2l0aCBUaGUgR0lNUAAh
- +QQBCgAfACwAAAAAJgAgAAAFsyAgjmRpnqgYCAPhvnAsz7BQAIJxIHzv/8Cg
- LyHA6YTI5I8IWLVo0Gjtlqpar9istqRYeL9exbaqYDTOaPRijFI40vDGmm16
- NB74NwOPh9C5DWIidn9VERIkb4UpEYIiZ4tZkJFWEA0MlFYLd5lVmw+dKZ8k
- fqEim4GnoKYAlndiDIisAG9ppawSaauzALkNsrzBwsPEIxMUFRVSyzQ2AAMW
- StJJTNDT10BMFwMYGczfUwAhADs=
- </icon>
- </objtype>
- <objtype name="thmset" descr="Set of Isabelle theorems">
- <contains objtype="theorem"/>
- </objtype>
-<!-- possible objtypes not yet supported:
- <objtype name="method" descr="Isar method or proof step"></objtype>
--->
-
- <!-- object operations -->
-
- <opn name="theory" descr="make a theory">
- <opsrc name="name">identifier</opsrc>
- <opsrc name="imports" listwithsep=" ">theory</opsrc>
- <optrg>theory</optrg>
- <opcmd>theory %name imports %imports begin
-
-end</opcmd>
- </opn>
-
- <opn name="open lemma">
- <inputform>
- <field name="name"><pgipstring/><prompt>Input a name:</prompt></field>
- <field name="term"><pgipstring/><prompt>Input a term:</prompt></field>
- <field name="attributes">
- <pgipchoice>
- <pgipconst name="" descr="none"></pgipconst>
- <pgipconst name="[simp]" descr="use in global simplifier context"></pgipconst>
- </pgipchoice>
- <prompt>Attributes:</prompt></field>
- </inputform>
- <opsrc></opsrc>
- <opcmd>lemma %attributes %name : "%term"
-sorry
-</opcmd>
- </opn>
-
-
- <opn name="add to simpset">
- <opsrc>theorem</opsrc>
- <optrg></optrg>
- <opcmd>declare %1 [simp]</opcmd>
- </opn>
-
- <opn name="remove from simpset">
- <opsrc>theorem</opsrc>
- <optrg></optrg>
- <opcmd>declare %1 [simp del]</opcmd>
- </opn>
-
- <opn name="instantiate" descr="instantiate variable in theorem">
- <opsrc>theorem</opsrc>
- <opsrc>term</opsrc>
- <optrg>theorem</optrg>
- <opcmd>%1 [OF %2]</opcmd>
- </opn>
-
- <!-- interactive operations -->
- <!-- da: this isn't really a good example.
- Isar doesn't have cterms, the "term" command just checks & prints
- a term in the current context. -->
- <opn name="checkterm">
- <inputform>
- <field name="term"><pgipstring/><prompt>Input a term:</prompt></field>
- </inputform>
- <opsrc></opsrc>
- <optrg>term</optrg>
- <opcmd>term %term</opcmd>
- </opn>
-
- <!-- proof operations -->
- <opn name="applyrule">
- <opsrc>ruleset</opsrc>
- <opcmd>apply (rule %1)</opcmd>
- </opn>
- <opn name="applyerule">
- <opsrc>ruleset</opsrc>
- <opcmd>apply (erule %1)</opcmd>
- </opn>
- <opn name="applydrule">
- <opsrc>ruleset</opsrc>
- <opcmd>apply (drule %1)</opcmd>
- </opn>
-
- <!-- introduce new goal -->
- <!-- [FIXME: ideally need to generalise substitution for options? in pgipchoice] -->
-
-
-</displayconfig>
-
--- 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* }
--- 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 @@
-<?xml version="1.0"?>
-<locatingRules xmlns="http://thaiopensource.com/ns/locating-rules/1.0">
- <uri resource="pgip_isar.xml" uri="pgip.rnc"/>
- <uri resource="pgip_isar.xml" typeId="RELAX NG"/>
-</locatingRules>
--- 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; )
--- 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
--- 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
--- 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
--- 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;
--- 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
--- 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))
*)
--- 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 "\<emdash>" 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 =>
--- 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
--- 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
--- 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 " ^
--- 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)
--- 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')
--- 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)
--- 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 = [];
--- 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
--- 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
--- 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 "<pgipnull/>");
-val _ = asseqx (pgiptype_to_xml Pgipbool) (XML.parse "<pgipbool/>");
-val _ = asseqx (pgiptype_to_xml (Pgipint (NONE,NONE))) (XML.parse "<pgipint/>");
-val _ = asseqx (pgiptype_to_xml (Pgipint (SOME 5,SOME 7))) (XML.parse "<pgipint min='5' max='7'/>");
-val _ = asseqx (pgiptype_to_xml (Pgipint (NONE,SOME 7))) (XML.parse "<pgipint max='7'/>");
-val _ = asseqx (pgiptype_to_xml (Pgipint (SOME ~5,NONE))) (XML.parse "<pgipint min='-5'/>");
-val _ = asseqx (pgiptype_to_xml Pgipstring) (XML.parse "<pgipstring/>");
-val _ = asseqx (pgiptype_to_xml (Pgipconst "radio1")) (XML.parse "<pgipconst name='radio1'/>");
-val _ = asseqx (pgiptype_to_xml (Pgipchoice [Pgipdtype (SOME "the best choice",Pgipbool)]))
- (XML.parse "<pgipchoice><pgipbool descr='the best choice'/></pgipchoice>");
-
-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 "<haspref name='provewithgusto' descr='use energetic proofs' default='true'><pgipbool/></haspref>");
-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 "<askpgip/>" (SOME (Askpgip()));
-val _ = asseqi "<askpgml/>" (SOME (Askpgml()));
-val _ = asseqi "<askconfig/>" (SOME (Askconfig()));
-(* FIXME: new tests:
-val _ = asseqi "<pgmlsymbolson/>" (SOME (Pgmlsymbolson()));
-val _ = asseqi "<pgmlsymbolsoff/>" (SOME (Pgmlsymbolsoff()));
-val _ = asseqi "<startquiet/>" (SOME (Startquiet()));
-val _ = asseqi "<stopquiet/>" (SOME (Stopquiet()));
-*)
-val _ = asseqi "<askrefs thyname='foo' objtype='theory'/>" (SOME (Askrefs {url=NONE, thyname=SOME "foo",
- objtype=SOME ObjTheory,name=NONE}));
-val _ = asseqi "<otherelt/>" 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
--- 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);
--- 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 "<forget> not implemented by Isabelle"
- | Pgip.Restoregoal _ => error "<restoregoal> 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 "<forget> not implemented by Isabelle"
+ | PgipInput.Restoregoal _ => error "<restoregoal> 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;
--- 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"
--- 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 *)
--- 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
--- 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;
--- 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
--- 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;
--- 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
--- 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,