--- a/Admin/ProofGeneral/3.7.1.1/interface Thu Oct 30 23:14:11 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,262 +0,0 @@
-#!/usr/bin/env bash
-#
-# interface,v 9.1 2008/02/06 15:40:45 makarius Exp
-#
-# Proof General interface wrapper for Isabelle.
-
-
-## self references
-
-THIS="$(cd "$(dirname "$0")"; pwd)"
-SUPER="$(cd "$THIS/.."; pwd)"
-
-
-## diagnostics
-
-usage()
-{
- echo
- echo "Usage: Isabelle [OPTIONS] [FILES ...]"
- echo
- echo " Options are:"
- echo " -I BOOL use Isabelle/Isar (default: true, implied by -P true)"
- echo " -L NAME abbreviates -l NAME -k NAME"
- echo " -P BOOL actually start Proof General (default true), otherwise"
- echo " run plain tty session"
- echo " -U BOOL enable Unicode (UTF-8) communication (default true)"
- echo " -X BOOL configure the X-Symbol package on startup (default true)"
- echo " -f SIZE set X-Symbol font size (default 12)"
- echo " -g GEOMETRY specify Emacs geometry"
- echo " -k NAME use specific isar-keywords for named logic"
- echo " -l NAME logic image name (default \$ISABELLE_LOGIC=$ISABELLE_LOGIC)"
- echo " -m MODE add print mode for output"
- echo " -p NAME Emacs program name (default emacs)"
- echo " -u BOOL use personal .emacs file (default true)"
- echo " -w BOOL use window system (default true)"
- echo " -x BOOL enable the X-Symbol package on startup (default false)"
- echo
- echo "Starts Proof General for Isabelle with theory and proof FILES"
- echo "(default Scratch.thy)."
- echo
- echo " PROOFGENERAL_OPTIONS=$PROOFGENERAL_OPTIONS"
- echo
- exit 1
-}
-
-fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-## process command line
-
-# options
-
-ISABELLE_OPTIONS=""
-ISAR="true"
-START_PG="true"
-GEOMETRY=""
-KEYWORDS=""
-LOGIC="$ISABELLE_LOGIC"
-PROGNAME="emacs"
-INITFILE="true"
-WINDOWSYSTEM="true"
-XSYMBOL=""
-XSYMBOL_SETUP=true
-XSYMBOL_FONTSIZE="12"
-UNICODE=""
-
-getoptions()
-{
- OPTIND=1
- while getopts "I:L:P:U:X:f:g:k:l:m:p:u:w:x:" OPT
- do
- case "$OPT" in
- I)
- ISAR="$OPTARG"
- ;;
- L)
- KEYWORDS="$OPTARG"
- LOGIC="$OPTARG"
- ;;
- P)
- START_PG="$OPTARG"
- ;;
- U)
- UNICODE="$OPTARG"
- ;;
- X)
- XSYMBOL_SETUP="$OPTARG"
- ;;
- f)
- XSYMBOL_FONTSIZE="$OPTARG"
- ;;
- g)
- GEOMETRY="$OPTARG"
- ;;
- k)
- KEYWORDS="$OPTARG"
- ;;
- l)
- LOGIC="$OPTARG"
- ;;
- m)
- if [ -z "$ISABELLE_OPTIONS" ]; then
- ISABELLE_OPTIONS="-m $OPTARG"
- else
- ISABELLE_OPTIONS="$ISABELLE_OPTIONS -m $OPTARG"
- fi
- ;;
- p)
- PROGNAME="$OPTARG"
- ;;
- u)
- INITFILE="$OPTARG"
- ;;
- w)
- WINDOWSYSTEM="$OPTARG"
- ;;
- x)
- XSYMBOL="$OPTARG"
- ;;
- \?)
- usage
- ;;
- esac
- done
-}
-
-eval "OPTIONS=($PROOFGENERAL_OPTIONS)"
-getoptions "${OPTIONS[@]}"
-
-getoptions "$@"
-shift $(($OPTIND - 1))
-
-
-# args
-
-declare -a FILES=()
-
-if [ "$#" -eq 0 ]; then
- FILES["${#FILES[@]}"]="Scratch.thy"
-else
- while [ "$#" -gt 0 ]; do
- FILES["${#FILES[@]}"]="$1"
- shift
- done
-fi
-
-
-## smart X11 font installation
-
-function checkfonts ()
-{
- XLSFONTS=$(xlsfonts -fn "-xsymb-xsymb0-*" 2>&1) || return 1
-
- case "$XLSFONTS" in
- xlsfonts:*)
- return 1
- ;;
- esac
-
- return 0
-}
-
-function installfonts ()
-{
- checkfonts "$XSYMBOL_PATTERN" || eval $XSYMBOL_INSTALLFONTS
-}
-
-
-## main
-
-# Isabelle2008 compatibility
-[ -z "$ISABELLE_PROCESS" ] && export ISABELLE_PROCESS="$ISABELLE"
-[ -z "$ISABELLE_TOOL" ] && export ISABELLE_TOOL="$ISATOOL"
-
-if [ "$START_PG" = false ]; then
-
- [ "$ISAR" = true ] && ISABELLE_OPTIONS="$ISABELLE_OPTIONS -I"
- exec "$ISABELLE_PROCESS" $ISABELLE_OPTIONS "$LOGIC"
-
-else
-
- declare -a ARGS=()
-
- if [ -n "$GEOMETRY" ]; then
- ARGS["${#ARGS[@]}"]="-geometry"
- ARGS["${#ARGS[@]}"]="$GEOMETRY"
- fi
-
- [ "$INITFILE" = false ] && ARGS["${#ARGS[@]}"]="-q"
-
- if [ "$WINDOWSYSTEM" = false ]; then
- ARGS["${#ARGS[@]}"]="-nw"
- XSYMBOL=false
- elif [ -z "$DISPLAY" ]; then
- XSYMBOL=false
- else
- [ -n "$XSYMBOL_INSTALLFONTS" -a "$XSYMBOL_SETUP" = true ] && installfonts
- fi
-
- if [ $(uname -s) = Darwin -a -d "$HOME/Library/Fonts" ]
- then
- if [ ! -f "$HOME/Library/Fonts/XSymb0Medium.ttf" -o ! -f "$HOME/Library/Fonts/XSymb1Medium.ttf" ]
- then
- cp -f "$SUPER/x-symbol/etc/fonts-ttf/XSymb0Medium.ttf" "$HOME/Library/Fonts/"
- cp -f "$SUPER/x-symbol/etc/fonts-ttf/XSymb1Medium.ttf" "$HOME/Library/Fonts/"
- sleep 3
- fi
- fi
-
- ARGS["${#ARGS[@]}"]="-l"
- ARGS["${#ARGS[@]}"]="$SUPER/isar/interface-setup.el"
-
- if [ -n "$KEYWORDS" ]; then
- if [ -f "$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" ]; then
- ARGS["${#ARGS[@]}"]="-l"
- ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el"
- elif [ -f "$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el" ]; then
- ARGS["${#ARGS[@]}"]="-l"
- ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el"
- else
- fail "No isar-keywords file for '$KEYWORDS'"
- fi
- elif [ -f "$ISABELLE_HOME_USER/etc/isar-keywords.el" ]; then
- ARGS["${#ARGS[@]}"]="-l"
- ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords.el"
- elif [ -f "$ISABELLE_HOME/etc/isar-keywords.el" ]; then
- ARGS["${#ARGS[@]}"]="-l"
- ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords.el"
- fi
-
- for FILE in "$ISABELLE_HOME/etc/proofgeneral-settings.el" \
- "$ISABELLE_HOME_USER/etc/proofgeneral-settings.el"
- do
- if [ -f "$FILE" ]; then
- ARGS["${#ARGS[@]}"]="-l"
- ARGS["${#ARGS[@]}"]="$FILE"
- fi
- done
-
- case "$LOGIC" in
- /*)
- ;;
- */*)
- LOGIC="$(pwd -P)/$LOGIC"
- ;;
- esac
-
- export PROOFGENERAL_HOME="$SUPER"
- export PROOFGENERAL_ASSISTANTS="isar"
- export PROOFGENERAL_LOGIC="$LOGIC"
- export PROOFGENERAL_XSYMBOL="$XSYMBOL"
- export PROOFGENERAL_UNICODE="$UNICODE"
-
- export ISABELLE_OPTIONS XSYMBOL_FONTSIZE
-
- exec "$PROGNAME" "${ARGS[@]}" "${FILES[@]}"
-
-fi
--- a/Admin/ProofGeneral/3.7.1.1/isar-antiq-regexp.patch Thu Oct 30 23:14:11 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
---- a/isar/isar-syntax.el Wed Aug 06 11:43:47 2008 +0200
-+++ b/isar/isar-syntax.el Thu Sep 18 15:21:16 2008 +0200
-@@ -252,14 +252,9 @@
-
- ;; antiquotations
-
--;; the \{0,10\} bound is there because otherwise font-lock sometimes hangs for
--;; incomplete antiquotations like @{text bla"} (even though it is supposed to
--;; stop at eol anyway).
--
--(defconst isar-antiq-regexp
-- (concat "@{\\(?:[^\"{}]+\\|" isar-string "\\)\\{0,10\\}}")
-- "Regexp matching Isabelle/Isar antiquoations.")
--
-+(defconst isar-antiq-regexp
-+ (concat "@{\\(?:[^\"{}]\\|" isar-string "\\)*}")
-+ "Regexp matching Isabelle/Isar antiquotations.")
-
- ;; keyword nesting
-
-
--- a/Admin/ProofGeneral/3.7.1.1/menu.patch Thu Oct 30 23:14:11 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
---- a/isar/isar.el 2008-07-10 20:47:49.000000000 +0200
-+++ b/isar/isar.el 2009-11-26 20:51:44.103016094 +0100
-@@ -339,9 +339,12 @@
- (error "Aborted."))
- [(control p)])
-
--(proof-definvisible isar-cmd-refute "refute" [r])
- (proof-definvisible isar-cmd-quickcheck "quickcheck" [(control q)])
-+(proof-definvisible isar-cmd-nitpick "nitpick" [(control n)])
-+(proof-definvisible isar-cmd-refute "refute" [r])
- (proof-definvisible isar-cmd-sledgehammer "sledgehammer" [(control s)])
-+(proof-definvisible isar-cmd-atp-kill "atp_kill")
-+(proof-definvisible isar-cmd-atp-info "atp_info")
-
- (defpgdefault menu-entries
- (append
-@@ -349,9 +352,12 @@
- (list
- (cons "Commands"
- (list
-- ["refute" isar-cmd-refute t]
- ["quickcheck" isar-cmd-quickcheck t]
-+ ["nitpick" isar-cmd-nitpick t]
-+ ["refute" isar-cmd-refute t]
- ["sledgehammer" isar-cmd-sledgehammer t]
-+ ["sledgehammer: kill" isar-cmd-atp-kill t]
-+ ["sledgehammer: info" isar-cmd-atp-info t]
- ["display draft" isar-cmd-display-draft t])))
- (list
- (cons "Show me ..."
--- a/Admin/ProofGeneral/3.7.1.1/progname.patch Thu Oct 30 23:14:11 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,89 +0,0 @@
---- a/isar/isabelle-system.el 2008-07-17 00:37:36.000000000 +0200
-+++ b/isar/isabelle-system.el 2009-11-30 17:06:05.508481278 +0100
-@@ -97,8 +97,8 @@
- (if (or proof-rsh-command
- (file-executable-p isa-isatool-command))
- (let ((setting (isa-shell-command-to-string
-- (concat isa-isatool-command
-- " getenv -b " envvar))))
-+ (concat "\"" isa-isatool-command
-+ "\" getenv -b " envvar))))
- (if (string-equal setting "")
- default
- setting))
-@@ -125,15 +125,12 @@
- :type 'file
- :group 'isabelle)
-
--(defvar isabelle-prog-name nil
-- "Set from `isabelle-set-prog-name', has name of logic appended sometimes.")
--
- (defun isa-tool-list-logics ()
- "Generate a list of available object logics."
- (if (isa-set-isatool-command)
- (delete "" (split-string
- (isa-shell-command-to-string
-- (concat isa-isatool-command " findlogics")) "[ \t]"))))
-+ (concat "\"" isa-isatool-command "\" findlogics")) "[ \t]"))))
-
- (defcustom isabelle-logics-available nil
- "*List of logics available to use with Isabelle.
-@@ -177,7 +174,7 @@
-
- (defun isabelle-set-prog-name (&optional filename)
- "Make proper command line for running Isabelle.
--This function sets `isabelle-prog-name' and `proof-prog-name'."
-+This function sets `proof-prog-name' and `isar-prog-args'."
- (let*
- ;; The ISABELLE and PROOFGENERAL_LOGIC values (set when run
- ;; under the interface wrapper script) indicate command line
-@@ -187,21 +184,20 @@
- (getenv "ISABELLE") ; command line override
- (isa-getenv "ISABELLE") ; choose to match isatool
- "isabelle")) ; to
-- (isabelle-opts (getenv "ISABELLE_OPTIONS"))
-- (opts (concat " -PI" ;; Proof General + Isar
-- (if proof-shell-unicode " -m PGASCII" "")
-- (if (and isabelle-opts (not (equal isabelle-opts "")))
-- (concat " " isabelle-opts) "")))
-+ (isabelle-opts (split-string (getenv "ISABELLE_OPTIONS")))
-+ (opts (append (list "-PI") ;; Proof General + Isar
-+ (if proof-shell-unicode (list "-m" "PGASCII") nil)
-+ isabelle-opts))
- (logic (or isabelle-chosen-logic
- (getenv "PROOFGENERAL_LOGIC")))
- (logicarg (if (and logic (not (equal logic "")))
-- (concat " " logic) "")))
-+ (list logic) nil)))
- (setq isabelle-chosen-logic-prev isabelle-chosen-logic)
-- (setq isabelle-prog-name (concat isabelle opts logicarg))
-- (setq proof-prog-name isabelle-prog-name)))
-+ (setq isar-prog-args (append opts logicarg))
-+ (setq proof-prog-name isabelle)))
-
- (defun isabelle-choose-logic (logic)
-- "Adjust isabelle-prog-name and proof-prog-name for running LOGIC."
-+ "Adjust proof-prog-name and isar-prog-args for running LOGIC."
- (interactive
- (list (completing-read
- "Use logic: "
-@@ -224,9 +220,7 @@
- (if (isa-set-isatool-command)
- (apply 'start-process
- "isa-view-doc" nil
-- (append (split-string
-- isa-isatool-command)
-- (list "doc" docname)))))
-+ (list isa-isatool-command "doc" docname))))
-
- (defun isa-tool-list-docs ()
- "Generate a list of documentation files available, with descriptions.
-@@ -236,7 +230,7 @@
- passed to isa-tool-doc-command, DOCNAME will be viewed."
- (if (isa-set-isatool-command)
- (let ((docs (isa-shell-command-to-string
-- (concat isa-isatool-command " doc"))))
-+ (concat "\"" isa-isatool-command "\" doc"))))
- (unless (string-equal docs "")
- (mapcan
- (function (lambda (docdes)
--- a/Admin/ProofGeneral/3.7.1.1/timeout.patch Thu Oct 30 23:14:11 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
---- a/generic/proof-config.el 2008-07-21 18:37:10.000000000 +0200
-+++ b/generic/proof-config.el 2009-11-29 17:41:37.409062091 +0100
-@@ -1493,7 +1493,7 @@
- :type '(choice string (const nil))
- :group 'proof-shell)
-
--(defcustom proof-shell-quit-timeout 4
-+(defcustom proof-shell-quit-timeout 45
- ;; FIXME could add option to quiz user before rude kill.
- "The number of seconds to wait after sending proof-shell-quit-cmd.
- After this timeout, the proof shell will be killed off more rudely.
--- a/Admin/ProofGeneral/3.7.1.1/version.patch Thu Oct 30 23:14:11 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
---- a/generic/proof-site.el 2008-07-23 14:40:14.000000000 +0200
-+++ b/generic/proof-site.el 2009-11-28 16:13:56.409505412 +0100
-@@ -55,7 +55,7 @@
-
- (eval-and-compile
- ;; WARNING: do not edit next line (constant is edited in Makefile.devel)
-- (defconst proof-general-version "Proof General Version 3.7.1. Released by da on Wed 23 Jul 2008."
-+ (defconst proof-general-version "Proof General Version 3.7.1.1. Fabricated by makarius on Mon 30 Nov 2009."
- "Version string identifying Proof General release."))
-
- (defconst proof-general-short-version
-@@ -64,7 +64,7 @@
- (string-match "Version \\([^ ]+\\)\\." proof-general-version)
- (match-string 1 proof-general-version))))
-
--(defconst proof-general-version-year "2008")
-+(defconst proof-general-version-year "2009")
-
- ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
- ;;
--- a/Admin/components/optional Thu Oct 30 23:14:11 2014 +0100
+++ b/Admin/components/optional Fri Oct 31 11:18:17 2014 +0100
@@ -1,3 +1,2 @@
#optional components that could impact build time significantly
hol-light-bundle-0.5-126
-ProofGeneral-4.2-2
--- a/Admin/lib/Tools/update_keywords Thu Oct 30 23:14:11 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: update standard keyword files for Emacs Proof General
-# (Proof General legacy)
-
-isabelle_admin_build jars || exit $?
-
-declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
-
-cd "$ISABELLE_HOME/etc"
-
-"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Keywords update_keywords
-
--- a/NEWS Thu Oct 30 23:14:11 2014 +0100
+++ b/NEWS Fri Oct 31 11:18:17 2014 +0100
@@ -187,6 +187,8 @@
*** System ***
+* Proof General support has been discontinued. Minor INCOMPATIBILITY.
+
* The Isabelle tool "update_cartouches" changes theory files to use
cartouches instead of old-style {* verbatim *} or `alt_string` tokens.
--- a/bin/isabelle_process Thu Oct 30 23:14:11 2014 +0100
+++ b/bin/isabelle_process Fri Oct 31 11:18:17 2014 +0100
@@ -28,7 +28,6 @@
echo " Options are:"
echo " -I startup Isar interaction mode"
echo " -O system options from given YXML file"
- echo " -P startup Proof General interaction mode"
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"
@@ -60,7 +59,6 @@
ISAR=""
OPTIONS_FILE=""
-PROOFGENERAL=""
SECURE=""
WRAPPER_SOCKET=""
WRAPPER_FIFOS=""
@@ -71,7 +69,7 @@
READONLY=""
NOWRITE=""
-while getopts "IO:PST:W:e:m:o:qrw" OPT
+while getopts "IO:ST:W:e:m:o:qrw" OPT
do
case "$OPT" in
I)
@@ -80,9 +78,6 @@
O)
OPTIONS_FILE="$OPTARG"
;;
- P)
- PROOFGENERAL=true
- ;;
S)
SECURE=true
;;
@@ -237,9 +232,7 @@
if [ "$INPUT" != RAW_ML_SYSTEM -a "$INPUT" != RAW ]; then
MLTEXT="Exn.capture_exit 2 Options.load_default (); $MLTEXT"
fi
- if [ -n "$PROOFGENERAL" ]; then
- MLTEXT="$MLTEXT; ProofGeneral.init ();"
- elif [ -n "$ISAR" ]; then
+ if [ -n "$ISAR" ]; then
MLTEXT="$MLTEXT; Isar.main ();"
else
NICE=""
--- a/etc/isar-keywords-ZF.el Thu Oct 30 23:14:11 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,502 +0,0 @@
-;;
-;; Keyword classification tables for Isabelle/Isar.
-;; Generated from Pure + ZF.
-;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
-;;
-
-(defconst isar-keywords-major
- '("\\."
- "\\.\\."
- "Isabelle\\.command"
- "ML"
- "ML_command"
- "ML_file"
- "ML_prf"
- "ML_val"
- "ProofGeneral\\.inform_file_processed"
- "ProofGeneral\\.inform_file_retracted"
- "ProofGeneral\\.kill_proof"
- "ProofGeneral\\.pr"
- "ProofGeneral\\.process_pgip"
- "ProofGeneral\\.restart"
- "ProofGeneral\\.undo"
- "SML_export"
- "SML_file"
- "SML_import"
- "abbreviation"
- "also"
- "apply"
- "apply_end"
- "assume"
- "attribute_setup"
- "axiomatization"
- "back"
- "bundle"
- "by"
- "cannot_undo"
- "case"
- "chapter"
- "class"
- "class_deps"
- "codatatype"
- "code_datatype"
- "coinductive"
- "commit"
- "consts"
- "context"
- "corollary"
- "datatype"
- "declaration"
- "declare"
- "def"
- "default_sort"
- "defer"
- "definition"
- "defs"
- "disable_pr"
- "display_drafts"
- "done"
- "enable_pr"
- "end"
- "exit"
- "extract"
- "extract_type"
- "finally"
- "find_consts"
- "find_theorems"
- "fix"
- "from"
- "full_prf"
- "guess"
- "have"
- "header"
- "help"
- "hence"
- "hide_class"
- "hide_const"
- "hide_fact"
- "hide_type"
- "include"
- "including"
- "inductive"
- "inductive_cases"
- "init_toplevel"
- "instance"
- "instantiation"
- "interpret"
- "interpretation"
- "judgment"
- "kill"
- "kill_thy"
- "lemma"
- "lemmas"
- "let"
- "linear_undo"
- "local_setup"
- "locale"
- "locale_deps"
- "method_setup"
- "moreover"
- "named_theorems"
- "next"
- "no_notation"
- "no_syntax"
- "no_translations"
- "no_type_notation"
- "nonterminal"
- "notation"
- "note"
- "notepad"
- "obtain"
- "oops"
- "oracle"
- "overloading"
- "parse_ast_translation"
- "parse_translation"
- "pr"
- "prefer"
- "presume"
- "pretty_setmargin"
- "prf"
- "primrec"
- "print_ML_antiquotations"
- "print_abbrevs"
- "print_antiquotations"
- "print_ast_translation"
- "print_attributes"
- "print_binds"
- "print_bundles"
- "print_cases"
- "print_claset"
- "print_classes"
- "print_codesetup"
- "print_commands"
- "print_context"
- "print_defn_rules"
- "print_dependencies"
- "print_facts"
- "print_induct_rules"
- "print_interps"
- "print_locale"
- "print_locales"
- "print_methods"
- "print_options"
- "print_rules"
- "print_simpset"
- "print_state"
- "print_statement"
- "print_syntax"
- "print_tcset"
- "print_term_bindings"
- "print_theorems"
- "print_theory"
- "print_trans_rules"
- "print_translation"
- "proof"
- "prop"
- "qed"
- "quit"
- "realizability"
- "realizers"
- "remove_thy"
- "rep_datatype"
- "schematic_corollary"
- "schematic_lemma"
- "schematic_theorem"
- "sect"
- "section"
- "setup"
- "show"
- "simproc_setup"
- "sorry"
- "subclass"
- "sublocale"
- "subsect"
- "subsection"
- "subsubsect"
- "subsubsection"
- "syntax"
- "syntax_declaration"
- "term"
- "text"
- "text_raw"
- "then"
- "theorem"
- "theorems"
- "theory"
- "thm"
- "thm_deps"
- "thus"
- "thy_deps"
- "translations"
- "txt"
- "txt_raw"
- "typ"
- "type_notation"
- "type_synonym"
- "typed_print_translation"
- "typedecl"
- "ultimately"
- "undo"
- "undos_proof"
- "unfolding"
- "unused_thms"
- "use_thy"
- "using"
- "welcome"
- "with"
- "write"
- "{"
- "}"))
-
-(defconst isar-keywords-minor
- '("and"
- "assumes"
- "attach"
- "begin"
- "binder"
- "case_eqns"
- "con_defs"
- "constrains"
- "defines"
- "domains"
- "elimination"
- "fixes"
- "for"
- "identifier"
- "if"
- "imports"
- "in"
- "includes"
- "induction"
- "infix"
- "infixl"
- "infixr"
- "intros"
- "is"
- "keywords"
- "monos"
- "notes"
- "obtains"
- "open"
- "output"
- "overloaded"
- "pervasive"
- "recursor_eqns"
- "shows"
- "structure"
- "type_elims"
- "type_intros"
- "unchecked"
- "where"))
-
-(defconst isar-keywords-control
- '("Isabelle\\.command"
- "ProofGeneral\\.inform_file_processed"
- "ProofGeneral\\.inform_file_retracted"
- "ProofGeneral\\.kill_proof"
- "ProofGeneral\\.pr"
- "ProofGeneral\\.process_pgip"
- "ProofGeneral\\.restart"
- "ProofGeneral\\.undo"
- "cannot_undo"
- "commit"
- "disable_pr"
- "enable_pr"
- "exit"
- "init_toplevel"
- "kill"
- "kill_thy"
- "linear_undo"
- "pretty_setmargin"
- "quit"
- "remove_thy"
- "undo"
- "undos_proof"
- "use_thy"))
-
-(defconst isar-keywords-diag
- '("ML_command"
- "ML_val"
- "class_deps"
- "display_drafts"
- "find_consts"
- "find_theorems"
- "full_prf"
- "header"
- "help"
- "locale_deps"
- "pr"
- "prf"
- "print_ML_antiquotations"
- "print_abbrevs"
- "print_antiquotations"
- "print_attributes"
- "print_binds"
- "print_bundles"
- "print_cases"
- "print_claset"
- "print_classes"
- "print_codesetup"
- "print_commands"
- "print_context"
- "print_defn_rules"
- "print_dependencies"
- "print_facts"
- "print_induct_rules"
- "print_interps"
- "print_locale"
- "print_locales"
- "print_methods"
- "print_options"
- "print_rules"
- "print_simpset"
- "print_state"
- "print_statement"
- "print_syntax"
- "print_tcset"
- "print_term_bindings"
- "print_theorems"
- "print_theory"
- "print_trans_rules"
- "prop"
- "term"
- "thm"
- "thm_deps"
- "thy_deps"
- "typ"
- "unused_thms"
- "welcome"))
-
-(defconst isar-keywords-theory-begin
- '("theory"))
-
-(defconst isar-keywords-theory-switch
- '())
-
-(defconst isar-keywords-theory-end
- '("end"))
-
-(defconst isar-keywords-theory-heading
- '("chapter"
- "section"
- "subsection"
- "subsubsection"))
-
-(defconst isar-keywords-theory-decl
- '("ML"
- "ML_file"
- "SML_export"
- "SML_file"
- "SML_import"
- "abbreviation"
- "attribute_setup"
- "axiomatization"
- "bundle"
- "class"
- "codatatype"
- "code_datatype"
- "coinductive"
- "consts"
- "context"
- "datatype"
- "declaration"
- "declare"
- "default_sort"
- "definition"
- "defs"
- "extract"
- "extract_type"
- "hide_class"
- "hide_const"
- "hide_fact"
- "hide_type"
- "inductive"
- "inductive_cases"
- "instantiation"
- "judgment"
- "lemmas"
- "local_setup"
- "locale"
- "method_setup"
- "named_theorems"
- "no_notation"
- "no_syntax"
- "no_translations"
- "no_type_notation"
- "nonterminal"
- "notation"
- "notepad"
- "oracle"
- "overloading"
- "parse_ast_translation"
- "parse_translation"
- "primrec"
- "print_ast_translation"
- "print_translation"
- "realizability"
- "realizers"
- "rep_datatype"
- "setup"
- "simproc_setup"
- "syntax"
- "syntax_declaration"
- "text"
- "text_raw"
- "theorems"
- "translations"
- "type_notation"
- "type_synonym"
- "typed_print_translation"
- "typedecl"))
-
-(defconst isar-keywords-theory-script
- '())
-
-(defconst isar-keywords-theory-goal
- '("corollary"
- "instance"
- "interpretation"
- "lemma"
- "schematic_corollary"
- "schematic_lemma"
- "schematic_theorem"
- "subclass"
- "sublocale"
- "theorem"))
-
-(defconst isar-keywords-qed
- '("\\."
- "\\.\\."
- "by"
- "done"
- "sorry"))
-
-(defconst isar-keywords-qed-block
- '("qed"))
-
-(defconst isar-keywords-qed-global
- '("oops"))
-
-(defconst isar-keywords-proof-heading
- '("sect"
- "subsect"
- "subsubsect"))
-
-(defconst isar-keywords-proof-goal
- '("have"
- "hence"
- "interpret"))
-
-(defconst isar-keywords-proof-block
- '("next"
- "proof"))
-
-(defconst isar-keywords-proof-open
- '("{"))
-
-(defconst isar-keywords-proof-close
- '("}"))
-
-(defconst isar-keywords-proof-chain
- '("finally"
- "from"
- "then"
- "ultimately"
- "with"))
-
-(defconst isar-keywords-proof-decl
- '("ML_prf"
- "also"
- "include"
- "including"
- "let"
- "moreover"
- "note"
- "txt"
- "txt_raw"
- "unfolding"
- "using"
- "write"))
-
-(defconst isar-keywords-proof-asm
- '("assume"
- "case"
- "def"
- "fix"
- "presume"))
-
-(defconst isar-keywords-proof-asm-goal
- '("guess"
- "obtain"
- "show"
- "thus"))
-
-(defconst isar-keywords-proof-script
- '("apply"
- "apply_end"
- "back"
- "defer"
- "prefer"))
-
-(provide 'isar-keywords)
--- a/etc/isar-keywords.el Thu Oct 30 23:14:11 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,718 +0,0 @@
-;;
-;; Keyword classification tables for Isabelle/Isar.
-;; Generated from HOL + HOL-Auth + HOL-Bali + HOL-Datatype_Examples + HOL-Decision_Procs + HOL-Hahn_Banach + HOL-IMP + HOL-Imperative_HOL + HOL-Import + HOL-Induct + HOL-Library + HOL-Multivariate_Analysis + HOL-Mutabelle + HOL-Nominal + HOL-Predicate_Compile_Examples + HOL-Probability + HOL-Proofs + HOL-Proofs-Extraction + HOL-SPARK + HOL-Statespace + HOL-TPTP + HOL-Word-SMT_Examples + HOL-ex + HOLCF + Pure.
-;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
-;;
-
-(defconst isar-keywords-major
- '("\\."
- "\\.\\."
- "Isabelle\\.command"
- "ML"
- "ML_command"
- "ML_file"
- "ML_prf"
- "ML_val"
- "ProofGeneral\\.inform_file_processed"
- "ProofGeneral\\.inform_file_retracted"
- "ProofGeneral\\.kill_proof"
- "ProofGeneral\\.pr"
- "ProofGeneral\\.process_pgip"
- "ProofGeneral\\.restart"
- "ProofGeneral\\.undo"
- "SML_export"
- "SML_file"
- "SML_import"
- "abbreviation"
- "adhoc_overloading"
- "also"
- "apply"
- "apply_end"
- "approximate"
- "assume"
- "atom_decl"
- "attribute_setup"
- "axiomatization"
- "back"
- "bnf"
- "bnf_axiomatization"
- "boogie_file"
- "bundle"
- "by"
- "cannot_undo"
- "cartouche"
- "case"
- "case_of_simps"
- "chapter"
- "class"
- "class_deps"
- "codatatype"
- "code_datatype"
- "code_deps"
- "code_identifier"
- "code_monad"
- "code_pred"
- "code_printing"
- "code_reflect"
- "code_reserved"
- "code_thms"
- "coinductive"
- "coinductive_set"
- "commit"
- "consts"
- "context"
- "corollary"
- "cpodef"
- "datatype"
- "datatype_compat"
- "declaration"
- "declare"
- "def"
- "default_sort"
- "defer"
- "defer_recdef"
- "definition"
- "defs"
- "disable_pr"
- "display_drafts"
- "domain"
- "domain_isomorphism"
- "domaindef"
- "done"
- "enable_pr"
- "end"
- "equivariance"
- "exit"
- "export_code"
- "extract"
- "extract_type"
- "finally"
- "find_consts"
- "find_theorems"
- "find_unused_assms"
- "fix"
- "fixrec"
- "free_constructors"
- "from"
- "full_prf"
- "fun"
- "fun_cases"
- "function"
- "functor"
- "guess"
- "have"
- "header"
- "help"
- "hence"
- "hide_class"
- "hide_const"
- "hide_fact"
- "hide_type"
- "import_const_map"
- "import_file"
- "import_tptp"
- "import_type_map"
- "include"
- "including"
- "inductive"
- "inductive_cases"
- "inductive_set"
- "inductive_simps"
- "init_toplevel"
- "instance"
- "instantiation"
- "interpret"
- "interpretation"
- "judgment"
- "kill"
- "kill_thy"
- "lemma"
- "lemmas"
- "let"
- "lift_definition"
- "lifting_forget"
- "lifting_update"
- "linear_undo"
- "local_setup"
- "locale"
- "locale_deps"
- "method_setup"
- "moreover"
- "named_theorems"
- "next"
- "nitpick"
- "nitpick_params"
- "no_adhoc_overloading"
- "no_notation"
- "no_syntax"
- "no_translations"
- "no_type_notation"
- "nominal_datatype"
- "nominal_function"
- "nominal_inductive"
- "nominal_inductive2"
- "nominal_primrec"
- "nominal_termination"
- "nonterminal"
- "notation"
- "note"
- "notepad"
- "obtain"
- "old_datatype"
- "old_rep_datatype"
- "old_smt_status"
- "oops"
- "oracle"
- "overloading"
- "parse_ast_translation"
- "parse_translation"
- "partial_function"
- "pcpodef"
- "permanent_interpretation"
- "pr"
- "prefer"
- "presume"
- "pretty_setmargin"
- "prf"
- "primcorec"
- "primcorecursive"
- "primrec"
- "print_ML_antiquotations"
- "print_abbrevs"
- "print_antiquotations"
- "print_ast_translation"
- "print_attributes"
- "print_binds"
- "print_bnfs"
- "print_bundles"
- "print_case_translations"
- "print_cases"
- "print_claset"
- "print_classes"
- "print_codeproc"
- "print_codesetup"
- "print_coercions"
- "print_commands"
- "print_context"
- "print_defn_rules"
- "print_dependencies"
- "print_facts"
- "print_induct_rules"
- "print_inductives"
- "print_interps"
- "print_locale"
- "print_locales"
- "print_methods"
- "print_options"
- "print_orders"
- "print_quot_maps"
- "print_quotconsts"
- "print_quotients"
- "print_quotientsQ3"
- "print_quotmapsQ3"
- "print_rules"
- "print_simpset"
- "print_state"
- "print_statement"
- "print_syntax"
- "print_term_bindings"
- "print_theorems"
- "print_theory"
- "print_trans_rules"
- "print_translation"
- "proof"
- "prop"
- "qed"
- "quickcheck"
- "quickcheck_generator"
- "quickcheck_params"
- "quit"
- "quotient_definition"
- "quotient_type"
- "realizability"
- "realizers"
- "recdef"
- "recdef_tc"
- "record"
- "refute"
- "refute_params"
- "remove_thy"
- "schematic_corollary"
- "schematic_lemma"
- "schematic_theorem"
- "sect"
- "section"
- "setup"
- "setup_lifting"
- "show"
- "simproc_setup"
- "simps_of_case"
- "sledgehammer"
- "sledgehammer_params"
- "smt_status"
- "solve_direct"
- "sorry"
- "spark_end"
- "spark_open"
- "spark_open_vcg"
- "spark_proof_functions"
- "spark_status"
- "spark_types"
- "spark_vc"
- "specification"
- "statespace"
- "subclass"
- "sublocale"
- "subsect"
- "subsection"
- "subsubsect"
- "subsubsection"
- "syntax"
- "syntax_declaration"
- "term"
- "term_cartouche"
- "termination"
- "test_code"
- "text"
- "text_cartouche"
- "text_raw"
- "then"
- "theorem"
- "theorems"
- "theory"
- "thm"
- "thm_deps"
- "thus"
- "thy_deps"
- "translations"
- "try"
- "try0"
- "txt"
- "txt_raw"
- "typ"
- "type_notation"
- "type_synonym"
- "typed_print_translation"
- "typedecl"
- "typedef"
- "ultimately"
- "undo"
- "undos_proof"
- "unfolding"
- "unused_thms"
- "use_thy"
- "using"
- "value"
- "values"
- "values_prolog"
- "welcome"
- "with"
- "write"
- "{"
- "}"))
-
-(defconst isar-keywords-minor
- '("and"
- "assumes"
- "attach"
- "avoids"
- "begin"
- "binder"
- "binds"
- "checking"
- "class_instance"
- "class_relation"
- "code_module"
- "congs"
- "constant"
- "constrains"
- "datatypes"
- "defines"
- "defining"
- "file"
- "fixes"
- "for"
- "functions"
- "hints"
- "identifier"
- "if"
- "imports"
- "in"
- "includes"
- "infix"
- "infixl"
- "infixr"
- "is"
- "keywords"
- "lazy"
- "module_name"
- "monos"
- "morphisms"
- "notes"
- "obtains"
- "open"
- "output"
- "overloaded"
- "parametric"
- "permissive"
- "pervasive"
- "shows"
- "structure"
- "type_class"
- "type_constructor"
- "unchecked"
- "unsafe"
- "where"))
-
-(defconst isar-keywords-control
- '("Isabelle\\.command"
- "ProofGeneral\\.inform_file_processed"
- "ProofGeneral\\.inform_file_retracted"
- "ProofGeneral\\.kill_proof"
- "ProofGeneral\\.pr"
- "ProofGeneral\\.process_pgip"
- "ProofGeneral\\.restart"
- "ProofGeneral\\.undo"
- "cannot_undo"
- "commit"
- "disable_pr"
- "enable_pr"
- "exit"
- "init_toplevel"
- "kill"
- "kill_thy"
- "linear_undo"
- "pretty_setmargin"
- "quit"
- "remove_thy"
- "undo"
- "undos_proof"
- "use_thy"))
-
-(defconst isar-keywords-diag
- '("ML_command"
- "ML_val"
- "approximate"
- "cartouche"
- "class_deps"
- "code_deps"
- "code_thms"
- "display_drafts"
- "find_consts"
- "find_theorems"
- "find_unused_assms"
- "full_prf"
- "header"
- "help"
- "locale_deps"
- "nitpick"
- "old_smt_status"
- "pr"
- "prf"
- "print_ML_antiquotations"
- "print_abbrevs"
- "print_antiquotations"
- "print_attributes"
- "print_binds"
- "print_bnfs"
- "print_bundles"
- "print_case_translations"
- "print_cases"
- "print_claset"
- "print_classes"
- "print_codeproc"
- "print_codesetup"
- "print_coercions"
- "print_commands"
- "print_context"
- "print_defn_rules"
- "print_dependencies"
- "print_facts"
- "print_induct_rules"
- "print_inductives"
- "print_interps"
- "print_locale"
- "print_locales"
- "print_methods"
- "print_options"
- "print_orders"
- "print_quot_maps"
- "print_quotconsts"
- "print_quotients"
- "print_quotientsQ3"
- "print_quotmapsQ3"
- "print_rules"
- "print_simpset"
- "print_state"
- "print_statement"
- "print_syntax"
- "print_term_bindings"
- "print_theorems"
- "print_theory"
- "print_trans_rules"
- "prop"
- "quickcheck"
- "refute"
- "sledgehammer"
- "smt_status"
- "solve_direct"
- "spark_status"
- "term"
- "term_cartouche"
- "test_code"
- "thm"
- "thm_deps"
- "thy_deps"
- "try"
- "try0"
- "typ"
- "unused_thms"
- "value"
- "values"
- "values_prolog"
- "welcome"))
-
-(defconst isar-keywords-theory-begin
- '("theory"))
-
-(defconst isar-keywords-theory-switch
- '())
-
-(defconst isar-keywords-theory-end
- '("end"))
-
-(defconst isar-keywords-theory-heading
- '("chapter"
- "section"
- "subsection"
- "subsubsection"))
-
-(defconst isar-keywords-theory-decl
- '("ML"
- "ML_file"
- "SML_export"
- "SML_file"
- "SML_import"
- "abbreviation"
- "adhoc_overloading"
- "atom_decl"
- "attribute_setup"
- "axiomatization"
- "bnf_axiomatization"
- "boogie_file"
- "bundle"
- "case_of_simps"
- "class"
- "codatatype"
- "code_datatype"
- "code_identifier"
- "code_monad"
- "code_printing"
- "code_reflect"
- "code_reserved"
- "coinductive"
- "coinductive_set"
- "consts"
- "context"
- "datatype"
- "datatype_compat"
- "declaration"
- "declare"
- "default_sort"
- "defer_recdef"
- "definition"
- "defs"
- "domain"
- "domain_isomorphism"
- "domaindef"
- "equivariance"
- "export_code"
- "extract"
- "extract_type"
- "fixrec"
- "fun"
- "fun_cases"
- "hide_class"
- "hide_const"
- "hide_fact"
- "hide_type"
- "import_const_map"
- "import_file"
- "import_tptp"
- "import_type_map"
- "inductive"
- "inductive_cases"
- "inductive_set"
- "inductive_simps"
- "instantiation"
- "judgment"
- "lemmas"
- "lifting_forget"
- "lifting_update"
- "local_setup"
- "locale"
- "method_setup"
- "named_theorems"
- "nitpick_params"
- "no_adhoc_overloading"
- "no_notation"
- "no_syntax"
- "no_translations"
- "no_type_notation"
- "nominal_datatype"
- "nonterminal"
- "notation"
- "notepad"
- "old_datatype"
- "oracle"
- "overloading"
- "parse_ast_translation"
- "parse_translation"
- "partial_function"
- "primcorec"
- "primrec"
- "print_ast_translation"
- "print_translation"
- "quickcheck_generator"
- "quickcheck_params"
- "realizability"
- "realizers"
- "recdef"
- "record"
- "refute_params"
- "setup"
- "setup_lifting"
- "simproc_setup"
- "simps_of_case"
- "sledgehammer_params"
- "spark_end"
- "spark_open"
- "spark_open_vcg"
- "spark_proof_functions"
- "spark_types"
- "statespace"
- "syntax"
- "syntax_declaration"
- "text"
- "text_cartouche"
- "text_raw"
- "theorems"
- "translations"
- "type_notation"
- "type_synonym"
- "typed_print_translation"
- "typedecl"))
-
-(defconst isar-keywords-theory-script
- '())
-
-(defconst isar-keywords-theory-goal
- '("bnf"
- "code_pred"
- "corollary"
- "cpodef"
- "free_constructors"
- "function"
- "functor"
- "instance"
- "interpretation"
- "lemma"
- "lift_definition"
- "nominal_function"
- "nominal_inductive"
- "nominal_inductive2"
- "nominal_primrec"
- "nominal_termination"
- "old_rep_datatype"
- "pcpodef"
- "permanent_interpretation"
- "primcorecursive"
- "quotient_definition"
- "quotient_type"
- "recdef_tc"
- "schematic_corollary"
- "schematic_lemma"
- "schematic_theorem"
- "spark_vc"
- "specification"
- "subclass"
- "sublocale"
- "termination"
- "theorem"
- "typedef"))
-
-(defconst isar-keywords-qed
- '("\\."
- "\\.\\."
- "by"
- "done"
- "sorry"))
-
-(defconst isar-keywords-qed-block
- '("qed"))
-
-(defconst isar-keywords-qed-global
- '("oops"))
-
-(defconst isar-keywords-proof-heading
- '("sect"
- "subsect"
- "subsubsect"))
-
-(defconst isar-keywords-proof-goal
- '("have"
- "hence"
- "interpret"))
-
-(defconst isar-keywords-proof-block
- '("next"
- "proof"))
-
-(defconst isar-keywords-proof-open
- '("{"))
-
-(defconst isar-keywords-proof-close
- '("}"))
-
-(defconst isar-keywords-proof-chain
- '("finally"
- "from"
- "then"
- "ultimately"
- "with"))
-
-(defconst isar-keywords-proof-decl
- '("ML_prf"
- "also"
- "include"
- "including"
- "let"
- "moreover"
- "note"
- "txt"
- "txt_raw"
- "unfolding"
- "using"
- "write"))
-
-(defconst isar-keywords-proof-asm
- '("assume"
- "case"
- "def"
- "fix"
- "presume"))
-
-(defconst isar-keywords-proof-asm-goal
- '("guess"
- "obtain"
- "show"
- "thus"))
-
-(defconst isar-keywords-proof-script
- '("apply"
- "apply_end"
- "back"
- "defer"
- "prefer"))
-
-(provide 'isar-keywords)
--- a/lib/Tools/keywords Thu Oct 30 23:14:11 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: generate keyword files for Emacs Proof General
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG [OPTIONS] [SESSIONS ...]"
- echo
- echo " Options are:"
- echo " -d DIR include session directory"
- echo " -k NAME specific name of keywords collection (default: empty)"
- echo
- echo " Generate keyword files for Emacs Proof General from Isabelle sessions."
- echo
- exit 1
-}
-
-
-## process command line
-
-# options
-
-declare -a DIRS=()
-KEYWORDS_NAME=""
-
-while getopts "d:k:" OPT
-do
- case "$OPT" in
- d)
- DIRS["${#DIRS[@]}"]="$OPTARG"
- ;;
- k)
- KEYWORDS_NAME="$OPTARG"
- ;;
- \?)
- usage
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
-
-
-## main
-
-isabelle_admin_build jars || exit $?
-
-declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
-
-"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Keywords keywords \
- "$KEYWORDS_NAME" "${DIRS[@]}" $'\n' "$@"
-
--- a/src/Doc/Classes/Classes.thy Thu Oct 30 23:14:11 2014 +0100
+++ b/src/Doc/Classes/Classes.thy Fri Oct 31 11:18:17 2014 +0100
@@ -179,8 +179,7 @@
primrec declaration; by default, the local name of a class operation
@{text f} to be instantiated on type constructor @{text \<kappa>} is
mangled as @{text f_\<kappa>}. In case of uncertainty, these names may be
- inspected using the @{command "print_context"} command or the
- corresponding ProofGeneral button.
+ inspected using the @{command "print_context"} command.
*}
subsection {* Lifting and parametric types *}
--- a/src/Doc/Implementation/ML.thy Thu Oct 30 23:14:11 2014 +0100
+++ b/src/Doc/Implementation/ML.thy Fri Oct 31 11:18:17 2014 +0100
@@ -1056,9 +1056,7 @@
\begin{warn}
The actual error channel is accessed via @{ML Output.error_message}, but
- the old interaction protocol of Proof~General \emph{crashes} if that
- function is used in regular ML code: error output and toplevel
- command failure always need to coincide in classic TTY interaction.
+ this is normally not used directly in user code.
\end{warn}
\end{description}
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Thu Oct 30 23:14:11 2014 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Fri Oct 31 11:18:17 2014 +0100
@@ -151,8 +151,7 @@
and sort constraints. This enables Prover IDE users to retrieve
that information via tooltips or popups while hovering with the
mouse over the output window, for example. Consequently, this
- option is enabled by default for Isabelle/jEdit, but disabled for
- TTY and Proof~General~/Emacs where document markup would not work.
+ option is enabled by default for Isabelle/jEdit.
\item @{attribute show_types} and @{attribute show_sorts} control
printing of type constraints for term variables, and sort
@@ -274,12 +273,6 @@
\end{description}
- \begin{warn}
- The old global reference @{ML print_mode} should never be used
- directly in applications. Its main reason for being publicly
- accessible is to support historic versions of Proof~General.
- \end{warn}
-
\medskip The pretty printer for inner syntax maintains alternative
mixfix productions for any print mode name invented by the user, say
in commands like @{command notation} or @{command abbreviation}.
@@ -299,9 +292,7 @@
\item @{verbatim xsymbols}: enable proper mathematical symbols
instead of ASCII art.\footnote{This traditional mode name stems from
- the ``X-Symbol'' package for old versions Proof~General with XEmacs,
- although that package has been superseded by Unicode in recent
- years.}
+ the ``X-Symbol'' package for classic Proof~General with XEmacs.}
\item @{verbatim HTML}: additional mode that is active in HTML
presentation of Isabelle theory sources; allows to provide
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Thu Oct 30 23:14:11 2014 +0100
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Fri Oct 31 11:18:17 2014 +0100
@@ -42,25 +42,10 @@
next command keyword.
More advanced interfaces such as Isabelle/jEdit @{cite "Wenzel:2012"}
- and Proof~General @{cite proofgeneral} do not require explicit
- semicolons: command spans are determined by inspecting the content
- of the editor buffer. In the printed presentation of Isabelle/Isar
- documents semicolons are omitted altogether for readability.
-
- \begin{warn}
- Proof~General requires certain syntax classification tables in
- order to achieve properly synchronized interaction with the
- Isabelle/Isar process. These tables need to be consistent with
- the Isabelle version and particular logic image to be used in a
- running session (common object-logics may well change the outer
- syntax). The standard setup should work correctly with any of the
- ``official'' logic images derived from Isabelle/HOL (including
- HOLCF etc.). Users of alternative logics may need to tell
- Proof~General explicitly, e.g.\ by giving an option @{verbatim "-k ZF"}
- (in conjunction with @{verbatim "-l ZF"}, to specify the default
- logic image). Note that option @{verbatim "-L"} does both
- of this at the same time.
- \end{warn}
+ do not require explicit semicolons: command spans are determined by
+ inspecting the content of the editor buffer. In the printed
+ presentation of Isabelle/Isar documents semicolons are omitted
+ altogether for readability.
\<close>
@@ -205,7 +190,7 @@
Common mathematical symbols such as @{text \<forall>} are represented in
Isabelle as @{verbatim \<forall>}. There are infinitely many Isabelle
symbols like this, although proper presentation is left to front-end
- tools such as {\LaTeX}, Proof~General, or Isabelle/jEdit. A list of
+ tools such as {\LaTeX} or Isabelle/jEdit. A list of
predefined Isabelle symbols that work well with these tools is given
in \appref{app:symbols}. Note that @{verbatim "\<lambda>"} does not belong
to the @{text letter} category, since it is already used differently
--- a/src/Doc/System/Basics.thy Thu Oct 30 23:14:11 2014 +0100
+++ b/src/Doc/System/Basics.thy Fri Oct 31 11:18:17 2014 +0100
@@ -363,7 +363,6 @@
Options are:
-I startup Isar interaction mode
-O system options from given YXML file
- -P startup Proof General interaction mode
-S secure mode -- disallow critical operations
-T ADDR startup process wrapper, with socket address
-W IN:OUT startup process wrapper, with input/output fifos
@@ -437,8 +436,6 @@
\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.
\medskip The @{verbatim "-T"} or @{verbatim "-W"} option makes
Isabelle enter a special process wrapper for interaction via
--- a/src/Doc/Tutorial/Documents/Documents.thy Thu Oct 30 23:14:11 2014 +0100
+++ b/src/Doc/Tutorial/Documents/Documents.thy Fri Oct 31 11:18:17 2014 +0100
@@ -102,9 +102,8 @@
Here $ident$ is any sequence of letters.
This results in an infinite store of symbols, whose
interpretation is left to further front-end tools. For example, the
- user-interface of Proof~General + X-Symbol and the Isabelle document
- processor (see \S\ref{sec:document-preparation}) display the
- \verb,\,\verb,<forall>, symbol as~@{text \<forall>}.
+ Isabelle document processor (see \S\ref{sec:document-preparation})
+ display the \verb,\,\verb,<forall>, symbol as~@{text \<forall>}.
A list of standard Isabelle symbols is given in
@{cite "isabelle-isar-ref"}. You may introduce your own
@@ -147,12 +146,7 @@
(*>*)
text {*
- \noindent Proof~General provides several input methods to enter
- @{text \<oplus>} in the text. If all fails one may just type a named
- entity \verb,\,\verb,<oplus>, by hand; the corresponding symbol will
- be displayed after further input.
-
- More flexible is to provide alternative syntax forms
+ It is possible to provide alternative syntax forms
through the \bfindex{print mode} concept~@{cite "isabelle-isar-ref"}. By
convention, the mode of ``$xsymbols$'' is enabled whenever
Proof~General's X-Symbol mode or {\LaTeX} output is active. Now
--- a/src/Doc/Tutorial/Types/Overloading.thy Thu Oct 30 23:14:11 2014 +0100
+++ b/src/Doc/Tutorial/Types/Overloading.thy Fri Oct 31 11:18:17 2014 +0100
@@ -37,8 +37,7 @@
suffix @{text "_nat"}; by default, the local name of a class operation
@{text f} to be instantiated on type constructor @{text \<kappa>} is mangled
as @{text f_\<kappa>}. In case of uncertainty, these names may be inspected
-using the @{command "print_context"} command or the corresponding
-ProofGeneral button.
+using the @{command "print_context"} command.
Although class @{class [source] plus} has no axioms, the instantiation must be
formally concluded by a (trivial) instantiation proof ``..'': *}
--- a/src/HOL/ROOT Thu Oct 30 23:14:11 2014 +0100
+++ b/src/HOL/ROOT Fri Oct 31 11:18:17 2014 +0100
@@ -600,7 +600,6 @@
Simps_Case_Conv_Examples
ML
SAT_Examples
- Nominal2_Dummy
SOS
SOS_Cert
theories [skip_proofs = false]
--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML Thu Oct 30 23:14:11 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML Fri Oct 31 11:18:17 2014 +0100
@@ -31,13 +31,6 @@
its time slot with several other automatic tools. *)
val auto_try_max_scopes = 6
-val _ =
- ProofGeneral.preference_option ProofGeneral.category_tracing
- NONE
- @{system_option auto_nitpick}
- "auto-nitpick"
- "Run Nitpick automatically"
-
type raw_param = string * string list
val default_default_params =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Oct 30 23:14:11 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Oct 31 11:18:17 2014 +0100
@@ -38,13 +38,6 @@
val running_learnersN = "running_learners"
val refresh_tptpN = "refresh_tptp"
-val _ =
- ProofGeneral.preference_option ProofGeneral.category_tracing
- NONE
- @{system_option auto_sledgehammer}
- "auto-sledgehammer"
- "Run Sledgehammer automatically"
-
(** Sledgehammer commands **)
fun add_fact_override ns : fact_override = {add = ns, del = [], only = false}
@@ -58,20 +51,6 @@
val provers = Unsynchronized.ref ""
-val _ =
- ProofGeneral.preference_string ProofGeneral.category_proof
- NONE
- provers
- "Sledgehammer: Provers"
- "Default automatic provers (separated by whitespace)"
-
-val _ =
- ProofGeneral.preference_option ProofGeneral.category_proof
- NONE
- @{system_option sledgehammer_timeout}
- "Sledgehammer: Time Limit"
- "ATPs will be interrupted after this time (in seconds)"
-
type raw_param = string * string list
val default_default_params =
--- a/src/HOL/Tools/try0.ML Thu Oct 30 23:14:11 2014 +0100
+++ b/src/HOL/Tools/try0.ML Fri Oct 31 11:18:17 2014 +0100
@@ -22,13 +22,6 @@
datatype mode = Auto_Try | Try | Normal;
-val _ =
- ProofGeneral.preference_option ProofGeneral.category_tracing
- NONE
- @{system_option auto_methods}
- "auto-try0"
- "Try standard proof methods";
-
val default_timeout = seconds 5.0;
fun can_apply timeout_opt pre post tac st =
--- a/src/HOL/ex/Nominal2_Dummy.thy Thu Oct 30 23:14:11 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-header \<open>Dummy theory to anticipate AFP/Nominal2 keywords\<close> (* Proof General legacy *)
-
-theory Nominal2_Dummy
-imports Main
-keywords
- "nominal_datatype" :: thy_decl and
- "nominal_function" "nominal_inductive" "nominal_termination" :: thy_goal and
- "atom_decl" "equivariance" :: thy_decl and
- "avoids" "binds"
-begin
-
-ML \<open>
-Outer_Syntax.command @{command_spec "nominal_datatype"} "dummy" Scan.fail;
-Outer_Syntax.command @{command_spec "nominal_function"} "dummy" Scan.fail;
-Outer_Syntax.command @{command_spec "nominal_inductive"} "dummy" Scan.fail;
-Outer_Syntax.command @{command_spec "nominal_termination"} "dummy" Scan.fail;
-Outer_Syntax.command @{command_spec "atom_decl"} "dummy" Scan.fail;
-Outer_Syntax.command @{command_spec "equivariance"} "dummy" Scan.fail;
-\<close>
-
-end
-
--- a/src/Pure/General/secure.ML Thu Oct 30 23:14:11 2014 +0100
+++ b/src/Pure/General/secure.ML Fri Oct 31 11:18:17 2014 +0100
@@ -13,7 +13,6 @@
val use_text: use_context -> int * string -> bool -> string -> unit
val use_file: use_context -> bool -> string -> unit
val toplevel_pp: string list -> string -> unit
- val PG_setup: unit -> unit
val commit: unit -> unit
end;
@@ -53,8 +52,5 @@
fun commit () = use_global "commit();"; (*commit is dynamically bound!*)
-fun PG_setup () =
- use_global "val change = Unsynchronized.change; structure ThyLoad = ProofGeneral.ThyLoad;";
-
end;
--- a/src/Pure/Pure.thy Thu Oct 30 23:14:11 2014 +0100
+++ b/src/Pure/Pure.thy Fri Oct 31 11:18:17 2014 +0100
@@ -100,9 +100,6 @@
and "extract_type" "extract" :: thy_decl
and "find_theorems" "find_consts" :: diag
and "named_theorems" :: thy_decl
- and "ProofGeneral.process_pgip" "ProofGeneral.pr" "ProofGeneral.undo"
- "ProofGeneral.restart" "ProofGeneral.kill_proof" "ProofGeneral.inform_file_processed"
- "ProofGeneral.inform_file_retracted" :: control
begin
ML_file "ML/ml_antiquotations.ML"
@@ -117,7 +114,6 @@
ML_file "Tools/class_deps.ML"
ML_file "Tools/find_theorems.ML"
ML_file "Tools/find_consts.ML"
-ML_file "Tools/proof_general_pure.ML"
ML_file "Tools/simplifier_trace.ML"
ML_file "Tools/named_theorems.ML"
--- a/src/Pure/ROOT Thu Oct 30 23:14:11 2014 +0100
+++ b/src/Pure/ROOT Fri Oct 31 11:18:17 2014 +0100
@@ -211,7 +211,6 @@
"Tools/build.ML"
"Tools/named_thms.ML"
"Tools/plugin.ML"
- "Tools/proof_general.ML"
"assumption.ML"
"axclass.ML"
"config.ML"
--- a/src/Pure/ROOT.ML Thu Oct 30 23:14:11 2014 +0100
+++ b/src/Pure/ROOT.ML Fri Oct 31 11:18:17 2014 +0100
@@ -334,7 +334,6 @@
use "Tools/build.ML";
use "Tools/named_thms.ML";
-use "Tools/proof_general.ML";
structure Output: OUTPUT = Output; (*seal system channels!*)
--- a/src/Pure/Tools/keywords.scala Thu Oct 30 23:14:11 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,179 +0,0 @@
-/* Title: Pure/Tools/keywords.scala
- Author: Makarius
-
-Generate keyword files for Emacs Proof General.
-*/
-
-/*Proof General legacy*/
-
-package isabelle
-
-
-import scala.collection.mutable
-
-
-object Keywords
-{
- /* keywords */
-
- private val convert = Map(
- "thy_begin" -> "theory-begin",
- "thy_end" -> "theory-end",
- "thy_heading1" -> "theory-heading",
- "thy_heading2" -> "theory-heading",
- "thy_heading3" -> "theory-heading",
- "thy_heading4" -> "theory-heading",
- "thy_load" -> "theory-decl",
- "thy_decl" -> "theory-decl",
- "thy_decl_block" -> "theory-decl",
- "thy_goal" -> "theory-goal",
- "qed_script" -> "qed",
- "qed_block" -> "qed-block",
- "qed_global" -> "qed-global",
- "prf_heading2" -> "proof-heading",
- "prf_heading3" -> "proof-heading",
- "prf_heading4" -> "proof-heading",
- "prf_goal" -> "proof-goal",
- "prf_block" -> "proof-block",
- "prf_open" -> "proof-open",
- "prf_close" -> "proof-close",
- "prf_chain" -> "proof-chain",
- "prf_decl" -> "proof-decl",
- "prf_asm" -> "proof-asm",
- "prf_asm_goal" -> "proof-asm-goal",
- "prf_asm_goal_script" -> "proof-asm-goal",
- "prf_script" -> "proof-script"
- ).withDefault((s: String) => s)
-
- private val emacs_kinds = List(
- "major",
- "minor",
- "control",
- "diag",
- "theory-begin",
- "theory-switch",
- "theory-end",
- "theory-heading",
- "theory-decl",
- "theory-script",
- "theory-goal",
- "qed",
- "qed-block",
- "qed-global",
- "proof-heading",
- "proof-goal",
- "proof-block",
- "proof-open",
- "proof-close",
- "proof-chain",
- "proof-decl",
- "proof-asm",
- "proof-asm-goal",
- "proof-script")
-
- def keywords(
- options: Options,
- name: String = "",
- dirs: List[Path] = Nil,
- sessions: List[String] = Nil)
- {
- val relevant_sessions =
- for {
- (name, content) <-
- Build.session_dependencies(options, false, dirs, sessions).deps.toList
- keywords = content.keywords
- if !keywords.isEmpty
- } yield (name, keywords)
-
- val keywords_raw =
- (Map.empty[String, Set[String]].withDefaultValue(Set.empty) /: relevant_sessions) {
- case (map, (_, ks)) =>
- (map /: ks) {
- case (m, (name, Some(((kind, _), _)), _)) =>
- m + (name -> (m(name) + convert(kind)))
- case (m, (name, None, _)) =>
- m + (name -> (m(name) + "minor"))
- }
- }
-
- val keywords_unique =
- for ((name, kinds) <- keywords_raw) yield {
- kinds.toList match {
- case List(kind) => (name, kind)
- case _ =>
- (kinds - "minor").toList match {
- case List(kind) => (name, kind)
- case _ =>
- error("Inconsistent declaration of keyword " + quote(name) + ": " +
- kinds.toList.sorted.mkString(" vs "))
- }
- }
- }
-
- val output =
- {
- val out = new mutable.StringBuilder
-
- out ++= ";;\n"
- out ++= ";; Keyword classification tables for Isabelle/Isar.\n"
- out ++= ";; Generated from " + relevant_sessions.map(_._1).sorted.mkString(" + ") + ".\n"
- out ++= ";; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***\n"
- out ++= ";;\n"
-
- for (kind <- emacs_kinds) {
- val names =
- (for {
- (name, k) <- keywords_unique.iterator
- if (if (kind == "major") k != "minor" else k == kind)
- if kind != "minor" || Symbol.is_ascii_identifier(name)
- } yield name).toList.sorted
-
- out ++= "\n(defconst isar-keywords-" + kind
- out ++= "\n '("
- out ++=
- names.map(name => quote("""[\.\*\+\?\[\]\^\$]""".r replaceAllIn (name, """\\\\$0""")))
- .mkString("\n ")
- out ++= "))\n"
- }
-
- out ++= "\n(provide 'isar-keywords)\n"
-
- out.toString
- }
-
- val file = if (name == "") "isar-keywords.el" else "isar-keywords-" + name + ".el"
- Output.writeln(file)
- File.write(Path.explode(file), output)
- }
-
-
- /* administrative update_keywords */
-
- def update_keywords(options: Options)
- {
- val tree = Build.find_sessions(options)
-
- def chapter(ch: String): List[String] =
- for ((name, info) <- tree.topological_order if info.chapter == ch) yield name
-
- keywords(options, sessions = chapter("HOL"))
- keywords(options, name = "ZF", sessions = chapter("ZF"))
- }
-
-
- /* command line entry point */
-
- def main(args: Array[String])
- {
- Command_Line.tool0 {
- args.toList match {
- case "keywords" :: name :: Command_Line.Chunks(dirs, sessions) =>
- keywords(Options.init(), name, dirs.map(Path.explode), sessions)
- case "update_keywords" :: Nil =>
- update_keywords(Options.init())
- case _ => error("Bad arguments:\n" + cat_lines(args))
- }
- }
- }
-}
-
--- a/src/Pure/Tools/proof_general.ML Thu Oct 30 23:14:11 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,443 +0,0 @@
-(* Title: Pure/Tools/proof_general.ML
- Author: David Aspinall
- Author: Makarius
-
-Isabelle/Isar configuration for Proof General / Emacs.
-See also http://proofgeneral.inf.ed.ac.uk
-*)
-
-(*Proof General legacy*)
-
-signature PROOF_GENERAL =
-sig
- type category = string
- val category_display: category
- val category_advanced_display: category
- val category_tracing: category
- val category_proof: category
- type pgiptype = string
- val pgipbool: pgiptype
- val pgipint: pgiptype
- val pgipfloat: pgiptype
- val pgipstring: pgiptype
- val preference: category -> string option ->
- (unit -> string) -> (string -> unit) -> string -> string -> string -> unit
- val preference_bool: category -> string option ->
- bool Unsynchronized.ref -> string -> string -> unit
- val preference_int: category -> string option ->
- int Unsynchronized.ref -> string -> string -> unit
- val preference_real: category -> string option ->
- real Unsynchronized.ref -> string -> string -> unit
- val preference_string: category -> string option ->
- string Unsynchronized.ref -> string -> string -> unit
- val preference_option: category -> string option -> string -> string -> string -> unit
- val process_pgip: string -> unit
- val tell_clear_goals: unit -> unit
- val tell_clear_response: unit -> unit
- val inform_file_processed: string -> unit
- val inform_file_retracted: string -> unit
- val master_path: Path.T Unsynchronized.ref
- structure ThyLoad: sig val add_path: string -> unit end
- val thm_deps: bool Unsynchronized.ref
- val proof_generalN: string
- val init: unit -> unit
- val restart: unit -> unit
-end;
-
-structure ProofGeneral: PROOF_GENERAL =
-struct
-
-(** preferences **)
-
-(* type preference *)
-
-type category = string;
-val category_display = "Display";
-val category_advanced_display = "Advanced Display";
-val category_tracing = "Tracing";
-val category_proof = "Proof";
-
-type pgiptype = string;
-val pgipbool = "pgipbool";
-val pgipint = "pgipint";
-val pgipfloat = "pgipint"; (*NB: PG 3.7.x and 4.0 lack pgipfloat, but accept floats as pgipint*)
-val pgipstring = "pgipstring";
-
-type preference =
- {category: string,
- override: string option,
- descr: string,
- pgiptype: pgiptype,
- get: unit -> string,
- set: string -> unit};
-
-
-(* global preferences *)
-
-local
- val preferences =
- Synchronized.var "ProofGeneral.preferences" ([]: (string * preference) list);
-in
-
-fun add_preference name pref =
- Synchronized.change preferences (fn prefs =>
- (if not (AList.defined (op =) prefs name) then ()
- else warning ("Redefining ProofGeneral preference: " ^ quote name);
- AList.update (op =) (name, pref) prefs));
-
-fun set_preference name value =
- (case AList.lookup (op =) (Synchronized.value preferences) name of
- SOME {set, ...} => set value
- | NONE => error ("Unknown ProofGeneral preference: " ^ quote name));
-
-fun all_preferences () =
- rev (Synchronized.value preferences)
- |> map (fn (name, {category, descr, pgiptype, get, ...}) =>
- (category, {name = name, descr = descr, default = get (), pgiptype = pgiptype}))
- |> AList.group (op =);
-
-fun init_preferences () =
- Synchronized.value preferences
- |> List.app (fn (_, {set, override = SOME value, ...}) => set value | _ => ());
-
-end;
-
-
-
-(* raw preferences *)
-
-fun preference category override get set typ name descr =
- add_preference name
- {category = category, override = override, descr = descr, pgiptype = typ, get = get, set = set};
-
-fun preference_ref category override read write typ r =
- preference category override (fn () => read (! r)) (fn x => r := write x) typ;
-
-fun preference_bool x y = preference_ref x y Markup.print_bool Markup.parse_bool pgipbool;
-fun preference_int x y = preference_ref x y Markup.print_int Markup.parse_int pgipint;
-fun preference_real x y = preference_ref x y Markup.print_real Markup.parse_real pgipfloat;
-fun preference_string x y = preference_ref x y I I pgipstring;
-
-
-(* system options *)
-
-fun preference_option category override option_name pgip_name descr =
- let
- val typ = Options.default_typ option_name;
- val pgiptype =
- if typ = Options.boolT then pgipbool
- else if typ = Options.intT then pgipint
- else if typ = Options.realT then pgipfloat
- else pgipstring;
- in
- add_preference pgip_name
- {category = category,
- override = override,
- descr = descr,
- pgiptype = pgiptype,
- get = fn () => Options.get_default option_name,
- set = Options.put_default option_name}
- end;
-
-
-(* minimal PGIP support for <askprefs>, <haspref>, <setpref> *)
-
-local
-
-fun get_attr attrs name =
- (case Properties.get attrs name of
- SOME value => value
- | NONE => raise Fail ("Missing attribute: " ^ quote name));
-
-fun attr x y = [(x, y)] : XML.attributes;
-
-fun opt_attr _ NONE = []
- | opt_attr name (SOME value) = attr name value;
-
-val pgip_id = "dummy";
-val pgip_serial = Counter.make ();
-
-fun output_pgip refid refseq content =
- XML.Elem (("pgip",
- attr "tag" "Isabelle/Isar" @
- attr "id" pgip_id @
- opt_attr "destid" refid @
- attr "class" "pg" @
- opt_attr "refid" refid @
- attr "refseq" refseq @
- attr "seq" (string_of_int (pgip_serial ()))), content)
- |> XML.string_of
- |> Output.urgent_message;
-
-
-fun invalid_pgip () = raise Fail "Invalid PGIP packet";
-
-fun haspref {name, descr, default, pgiptype} =
- XML.Elem (("haspref", [("name", name), ("descr", descr), ("default", default)]),
- [XML.Elem ((pgiptype, []), [])]);
-
-fun process_element refid refseq (XML.Elem (("askprefs", _), _)) =
- all_preferences () |> List.app (fn (category, prefs) =>
- output_pgip refid refseq
- [XML.Elem (("hasprefs", [("prefcategory", category)]), map haspref prefs)])
- | process_element _ _ (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 _ _ _ = invalid_pgip ();
-
-in
-
-fun process_pgip str =
- (case XML.parse str of
- XML.Elem (("pgip", attrs), pgips) =>
- let
- val class = get_attr attrs "class";
- val dest = Properties.get attrs "destid";
- val refid = Properties.get attrs "id";
- val refseq = get_attr attrs "seq";
- val processit =
- (case dest of
- NONE => class = "pa"
- | SOME id => id = pgip_id);
- in if processit then List.app (process_element refid refseq) pgips else () end
- | _ => invalid_pgip ())
- handle Fail msg => raise Fail (msg ^ "\n" ^ str);
-
-end;
-
-
-(** messages **)
-
-(* render markup *)
-
-fun special ch = chr 1 ^ ch;
-
-local
-
-fun render_trees ts = fold render_tree ts
-and render_tree t =
- (case XML.unwrap_elem t of
- SOME (_, ts) => render_trees ts
- | NONE =>
- (case t of
- XML.Text s => Buffer.add s
- | XML.Elem ((name, props), ts) =>
- let
- val (bg, en) =
- if null ts then Markup.no_output
- else if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
- else if name = Markup.sendbackN then (special "W", special "X")
- else if name = Markup.intensifyN then (special "0", special "1")
- else if name = Markup.informationN then ("\n" ^ special "0", special "1")
- else if name = Markup.tfreeN then (special "C", special "A")
- else if name = Markup.tvarN then (special "D", special "A")
- else if name = Markup.freeN then (special "E", special "A")
- else if name = Markup.boundN then (special "F", special "A")
- else if name = Markup.varN then (special "G", special "A")
- else if name = Markup.skolemN then (special "H", special "A")
- else
- (case Markup.get_entity_kind (name, props) of
- SOME kind =>
- if kind = Markup.classN then (special "B", special "A")
- else Markup.no_output
- | NONE => Markup.no_output);
- in Buffer.add bg #> render_trees ts #> Buffer.add en end));
-
-in
-
-fun render text =
- Buffer.content (render_trees (YXML.parse_body text) Buffer.empty);
-
-end;
-
-
-(* hooks *)
-
-fun message bg en prfx body =
- (case render (implode body) of
- "" => ()
- | s => Output.physical_writeln (enclose bg en (prefix_lines prfx s)));
-
-fun setup_messages () =
- (Output.writeln_fn := message "" "" "";
- Output.status_fn := (fn _ => ());
- Output.report_fn := (fn _ => ());
- Output.urgent_message_fn := message (special "I") (special "J") "";
- Output.tracing_fn := message (special "I" ^ special "V") (special "J") "";
- Output.warning_fn := message (special "K") (special "L") "### ";
- Output.error_message_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
- Output.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S")));
-
-
-(* notification *)
-
-fun emacs_notify s = message (special "I") (special "J") "" [s];
-
-fun tell_clear_goals () =
- emacs_notify "Proof General, please clear the goals buffer.";
-
-fun tell_clear_response () =
- emacs_notify "Proof General, please clear the response buffer.";
-
-fun tell_file_loaded path =
- emacs_notify ("Proof General, this file is loaded: " ^ quote (File.platform_path path));
-
-fun tell_file_retracted path =
- emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path));
-
-
-
-(** theory loader **)
-
-(* global master path *)
-
-val master_path = Unsynchronized.ref Path.current;
-
-(*fake old ThyLoad -- with new semantics*)
-structure ThyLoad =
-struct
- fun add_path path = master_path := Path.explode path;
-end;
-
-
-(* actions *)
-
-local
-
-fun trace_action action name =
- if action = Thy_Info.Update then
- List.app tell_file_loaded (Thy_Info.loaded_files name)
- else if action = Thy_Info.Remove then
- List.app tell_file_retracted (Thy_Info.loaded_files name)
- else ();
-
-in
- fun setup_thy_loader () = Thy_Info.add_hook trace_action;
- fun sync_thy_loader () = List.app (trace_action Thy_Info.Update) (Thy_Info.get_names ());
-end;
-
-
-(* get informed about files *)
-
-(*liberal low-level version*)
-val thy_name = perhaps (try (unsuffix ".thy")) o List.last o space_explode "/";
-
-val inform_file_retracted = Thy_Info.kill_thy o thy_name;
-
-fun inform_file_processed file =
- let
- val name = thy_name file;
- val _ = name = "" andalso error ("Bad file name: " ^ quote file);
- val _ =
- Thy_Info.register_thy (Toplevel.end_theory Position.none (Isar.state ()))
- handle ERROR msg =>
- (warning (cat_lines ["Failed to register theory: " ^ quote name, msg]);
- tell_file_retracted (Resources.thy_path (Path.basic name)))
- val _ = Isar.init ();
- in () end;
-
-
-
-(** theorem dependencies **)
-
-(* thm_deps *)
-
-local
-
-fun add_proof_body (PBody {thms, ...}) =
- thms |> fold (fn (_, (name, _, _)) => name <> "" ? Symtab.update (name, ()));
-
-fun add_thm th =
- (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)
- else I
- | body => add_proof_body body);
-
-in
-
-fun get_thm_deps ths =
- let
- (* FIXME proper derivation names!? *)
- val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
- val deps = Symtab.keys (fold add_thm ths Symtab.empty);
- in (names, deps) end;
-
-end;
-
-
-(* report via hook *)
-
-val thm_deps = Unsynchronized.ref false;
-
-local
-
-val spaces_quote = space_implode " " o map quote;
-
-fun thm_deps_message (thms, deps) =
- emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps);
-
-in
-
-fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn state' =>
- if ! thm_deps andalso can Toplevel.theory_of state andalso Toplevel.is_theory state'
- then
- let
- val prev_facts = Global_Theory.facts_of (Toplevel.theory_of state);
- val facts = Global_Theory.facts_of (Toplevel.theory_of state');
- val (names, deps) = get_thm_deps (maps #2 (Facts.dest_static true [prev_facts] facts));
- in
- if null names orelse null deps then ()
- else thm_deps_message (spaces_quote names, spaces_quote deps)
- end
- else ());
-
-end;
-
-
-
-(** startup **)
-
-(* init *)
-
-val proof_generalN = "ProofGeneral";
-
-val initialized = Unsynchronized.ref false;
-
-fun init () =
- (if ! initialized then ()
- else
- (Output.add_mode Symbol.xsymbolsN Symbol.output Output.default_escape;
- Output.add_mode proof_generalN Output.default_output Output.default_escape;
- Markup.add_mode proof_generalN YXML.output_markup;
- setup_messages ();
- setup_thy_loader ();
- setup_present_hook ();
- initialized := true);
- init_preferences ();
- sync_thy_loader ();
- Unsynchronized.change print_mode (update (op =) proof_generalN);
- Secure.PG_setup ();
- Isar.toplevel_loop TextIO.stdIn
- {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
-
-
-(* restart *)
-
-val welcome = Output.urgent_message o Session.welcome;
-
-fun restart () =
- (sync_thy_loader ();
- tell_clear_goals ();
- tell_clear_response ();
- Isar.init ();
- welcome ());
-
-end;
-
--- a/src/Pure/build-jars Thu Oct 30 23:14:11 2014 +0100
+++ b/src/Pure/build-jars Fri Oct 31 11:18:17 2014 +0100
@@ -90,7 +90,6 @@
Tools/build_doc.scala
Tools/check_source.scala
Tools/doc.scala
- Tools/keywords.scala
Tools/main.scala
Tools/ml_statistics.scala
Tools/print_operation.scala
--- a/src/Pure/pure_syn.ML Thu Oct 30 23:14:11 2014 +0100
+++ b/src/Pure/pure_syn.ML Fri Oct 31 11:18:17 2014 +0100
@@ -11,8 +11,7 @@
Outer_Syntax.command
(("theory", Keyword.tag_theory Keyword.thy_begin), @{here}) "begin theory"
(Thy_Header.args >> (fn header =>
- Toplevel.init_theory
- (fn () => Thy_Info.toplevel_begin_theory (! ProofGeneral.master_path) header)));
+ Toplevel.init_theory (fn () => Thy_Info.toplevel_begin_theory Path.current header)));
val _ =
Outer_Syntax.command
--- a/src/Tools/quickcheck.ML Thu Oct 30 23:14:11 2014 +0100
+++ b/src/Tools/quickcheck.ML Fri Oct 31 11:18:17 2014 +0100
@@ -90,16 +90,6 @@
val unknownN = "unknown";
-(* preferences *)
-
-val _ =
- ProofGeneral.preference_option ProofGeneral.category_tracing
- NONE
- @{system_option auto_quickcheck}
- "auto-quickcheck"
- "Run Quickcheck automatically";
-
-
(* quickcheck report *)
datatype report = Report of
--- a/src/Tools/solve_direct.ML Thu Oct 30 23:14:11 2014 +0100
+++ b/src/Tools/solve_direct.ML Fri Oct 31 11:18:17 2014 +0100
@@ -34,13 +34,6 @@
val max_solutions = Unsynchronized.ref 5;
-val _ =
- ProofGeneral.preference_option ProofGeneral.category_tracing
- NONE
- @{system_option auto_solve_direct}
- "auto-solve-direct"
- ("Run " ^ quote solve_directN ^ " automatically");
-
(* solve_direct command *)
--- a/src/Tools/try.ML Thu Oct 30 23:14:11 2014 +0100
+++ b/src/Tools/try.ML Fri Oct 31 11:18:17 2014 +0100
@@ -27,16 +27,6 @@
val tryN = "try"
-(* preferences *)
-
-val _ =
- ProofGeneral.preference_option ProofGeneral.category_tracing
- (SOME "4.0")
- @{system_option auto_time_limit}
- "auto-try-time-limit"
- "Time limit for automatically tried tools (in seconds)"
-
-
(* helpers *)
fun serial_commas _ [] = ["??"]