# HG changeset patch # User wenzelm # Date 1368290738 -7200 # Node ID f196352201d678c9cb115a713bf3ec1b195a2d41 # Parent 7c517c92d31525dfb2b5161cd9324007fd18f8d6 removed some obsolete PGIP/PGEclipse material; diff -r 7c517c92d315 -r f196352201d6 bin/isabelle-process --- a/bin/isabelle-process Sat May 11 18:16:17 2013 +0200 +++ b/bin/isabelle-process Sat May 11 18:45:38 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 7c517c92d315 -r f196352201d6 lib/ProofGeneral/README --- a/lib/ProofGeneral/README Sat May 11 18:16:17 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 7c517c92d315 -r f196352201d6 lib/ProofGeneral/pgip.rnc --- a/lib/ProofGeneral/pgip.rnc Sat May 11 18:16:17 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 7c517c92d315 -r f196352201d6 lib/ProofGeneral/pgip_isar.xml --- a/lib/ProofGeneral/pgip_isar.xml Sat May 11 18:16:17 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 7c517c92d315 -r f196352201d6 lib/ProofGeneral/pgml.rnc --- a/lib/ProofGeneral/pgml.rnc Sat May 11 18:16:17 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 7c517c92d315 -r f196352201d6 lib/ProofGeneral/schemas.xml --- a/lib/ProofGeneral/schemas.xml Sat May 11 18:16:17 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,5 +0,0 @@ - - - - - diff -r 7c517c92d315 -r f196352201d6 lib/Tools/mkproject --- a/lib/Tools/mkproject Sat May 11 18:16:17 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 7c517c92d315 -r f196352201d6 src/Doc/System/Basics.thy --- a/src/Doc/System/Basics.thy Sat May 11 18:16:17 2013 +0200 +++ b/src/Doc/System/Basics.thy Sat May 11 18:45:38 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 7c517c92d315 -r f196352201d6 src/Pure/ProofGeneral/TODO --- a/src/Pure/ProofGeneral/TODO Sat May 11 18:16:17 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