--- a/Admin/ProofGeneral/3.7.1.1/interface Fri Oct 31 17:01:54 2014 +0000
+++ /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 Fri Oct 31 17:01:54 2014 +0000
+++ /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 Fri Oct 31 17:01:54 2014 +0000
+++ /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 Fri Oct 31 17:01:54 2014 +0000
+++ /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 Fri Oct 31 17:01:54 2014 +0000
+++ /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 Fri Oct 31 17:01:54 2014 +0000
+++ /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 Fri Oct 31 17:01:54 2014 +0000
+++ b/Admin/components/optional Fri Oct 31 23:51:54 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 Fri Oct 31 17:01:54 2014 +0000
+++ /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 Fri Oct 31 17:01:54 2014 +0000
+++ b/NEWS Fri Oct 31 23:51:54 2014 +0100
@@ -187,6 +187,9 @@
*** System ***
+* Support for Proof General and Isar TTY loop 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 Fri Oct 31 17:01:54 2014 +0000
+++ b/bin/isabelle_process Fri Oct 31 23:51:54 2014 +0100
@@ -26,9 +26,7 @@
echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
echo
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"
@@ -58,9 +56,7 @@
# options
-ISAR=""
OPTIONS_FILE=""
-PROOFGENERAL=""
SECURE=""
WRAPPER_SOCKET=""
WRAPPER_FIFOS=""
@@ -71,18 +67,12 @@
READONLY=""
NOWRITE=""
-while getopts "IO:PST:W:e:m:o:qrw" OPT
+while getopts "O:ST:W:e:m:o:qrw" OPT
do
case "$OPT" in
- I)
- ISAR=true
- ;;
O)
OPTIONS_FILE="$OPTARG"
;;
- P)
- PROOFGENERAL=true
- ;;
S)
SECURE=true
;;
@@ -213,8 +203,6 @@
[ -n "$SECURE" ] && MLTEXT="$MLTEXT; Secure.set_secure ();"
-NICE="nice"
-
if [ -n "$WRAPPER_SOCKET" ]; then
MLTEXT="$MLTEXT; Isabelle_Process.init_socket \"$WRAPPER_SOCKET\";"
elif [ -n "$WRAPPER_FIFOS" ]; then
@@ -237,21 +225,14 @@
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
- MLTEXT="$MLTEXT; Isar.main ();"
- else
- NICE=""
- fi
fi
export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_PID ISABELLE_TMP ISABELLE_PROCESS_OPTIONS
if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
- $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
+ "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
else
- $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
+ "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
fi
RC="$?"
--- a/etc/isar-keywords-ZF.el Fri Oct 31 17:01:54 2014 +0000
+++ /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 Fri Oct 31 17:01:54 2014 +0000
+++ /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/etc/options Fri Oct 31 17:01:54 2014 +0000
+++ b/etc/options Fri Oct 31 23:51:54 2014 +0100
@@ -90,9 +90,6 @@
option condition : string = ""
-- "required environment variables for subsequent theories (separated by commas)"
-option timing : bool = false
- -- "global timing of toplevel command execution and theory processing"
-
option timeout : real = 0
-- "timeout for session build job (seconds > 0)"
--- a/lib/Tools/keywords Fri Oct 31 17:01:54 2014 +0000
+++ /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 Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Doc/Classes/Classes.thy Fri Oct 31 23:51:54 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 Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Doc/Implementation/ML.thy Fri Oct 31 23:51:54 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 Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Fri Oct 31 23:51:54 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 Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Fri Oct 31 23:51:54 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 Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Doc/System/Basics.thy Fri Oct 31 23:51:54 2014 +0100
@@ -361,9 +361,7 @@
Usage: isabelle_process [OPTIONS] [INPUT] [OUTPUT]
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
@@ -435,11 +433,6 @@
system options as a file in YXML format (according to the Isabelle/Scala
function @{verbatim isabelle.Options.encode}).
- \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
Isabelle/Scala, see also @{file
--- a/src/Doc/Tutorial/Documents/Documents.thy Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Doc/Tutorial/Documents/Documents.thy Fri Oct 31 23:51:54 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/ToyList/ToyList_Test.thy Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Doc/Tutorial/ToyList/ToyList_Test.thy Fri Oct 31 23:51:54 2014 +0100
@@ -3,10 +3,11 @@
begin
ML {*
- map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode)
- ["ToyList1.txt", "ToyList2.txt"]
- |> implode
- |> Thy_Info.script_thy Position.start
+ let val text =
+ map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode)
+ ["ToyList1.txt", "ToyList2.txt"]
+ |> implode
+ in Thy_Info.script_thy Position.start text @{theory BNF_Least_Fixpoint} end
*}
end
--- a/src/Doc/Tutorial/Types/Overloading.thy Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Doc/Tutorial/Types/Overloading.thy Fri Oct 31 23:51:54 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/Divides.thy Fri Oct 31 17:01:54 2014 +0000
+++ b/src/HOL/Divides.thy Fri Oct 31 23:51:54 2014 +0100
@@ -2047,8 +2047,8 @@
val less = @{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"}
val le = @{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"}
val simps = @{thms arith_simps} @ @{thms rel_simps} @ [@{thm numeral_1_eq_1 [symmetric]}]
- fun prove ctxt goal = (writeln "prove"; Goal.prove ctxt [] [] (HOLogic.mk_Trueprop goal)
- (K (ALLGOALS (full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps)))));
+ fun prove ctxt goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop goal)
+ (K (ALLGOALS (full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps))));
fun binary_proc proc ctxt ct =
(case Thm.term_of ct of
_ $ t $ u =>
--- a/src/HOL/Library/refute.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/HOL/Library/refute.ML Fri Oct 31 23:51:54 2014 +0100
@@ -1068,31 +1068,31 @@
". Available solvers: " ^
commas (map (quote o fst) (SAT_Solver.get_solvers ())) ^ ".")
in
- Output.urgent_message "Invoking SAT solver...";
+ writeln "Invoking SAT solver...";
(case solver fm of
SAT_Solver.SATISFIABLE assignment =>
- (Output.urgent_message ("Model found:\n" ^ print_model ctxt model
+ (writeln ("Model found:\n" ^ print_model ctxt model
(fn i => case assignment i of SOME b => b | NONE => true));
if maybe_spurious then "potential" else "genuine")
| SAT_Solver.UNSATISFIABLE _ =>
- (Output.urgent_message "No model exists.";
+ (writeln "No model exists.";
case next_universe universe sizes minsize maxsize of
SOME universe' => find_model_loop universe'
- | NONE => (Output.urgent_message
+ | NONE => (writeln
"Search terminated, no larger universe within the given limits.";
"none"))
| SAT_Solver.UNKNOWN =>
- (Output.urgent_message "No model found.";
+ (writeln "No model found.";
case next_universe universe sizes minsize maxsize of
SOME universe' => find_model_loop universe'
- | NONE => (Output.urgent_message
+ | NONE => (writeln
"Search terminated, no larger universe within the given limits.";
"unknown"))) handle SAT_Solver.NOT_CONFIGURED =>
(error ("SAT solver " ^ quote satsolver ^ " is not configured.");
"unknown")
end
handle MAXVARS_EXCEEDED =>
- (Output.urgent_message ("Search terminated, number of Boolean variables ("
+ (writeln ("Search terminated, number of Boolean variables ("
^ string_of_int maxvars ^ " allowed) exceeded.");
"unknown")
@@ -1114,14 +1114,14 @@
maxtime>=0 orelse
error ("\"maxtime\" is " ^ string_of_int maxtime ^ ", must be at least 0");
(* enter loop with or without time limit *)
- Output.urgent_message ("Trying to find a model that "
+ writeln ("Trying to find a model that "
^ (if negate then "refutes" else "satisfies") ^ ": "
^ Syntax.string_of_term ctxt t);
if maxtime > 0 then (
TimeLimit.timeLimit (Time.fromSeconds maxtime)
wrapper ()
handle TimeLimit.TimeOut =>
- (Output.urgent_message ("Search terminated, time limit (" ^
+ (writeln ("Search terminated, time limit (" ^
string_of_int maxtime
^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.");
check_expect "unknown")
@@ -1207,7 +1207,7 @@
val t = th |> prop_of
in
if Logic.count_prems t = 0 then
- (Output.urgent_message "No subgoal!"; "none")
+ (writeln "No subgoal!"; "none")
else
let
val assms = map term_of (Assumption.all_assms_of ctxt)
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Oct 31 23:51:54 2014 +0100
@@ -428,7 +428,7 @@
|> tap (fn factss =>
"Line " ^ str0 (Position.line_of pos) ^ ": " ^
Sledgehammer.string_of_factss factss
- |> Output.urgent_message)
+ |> writeln)
val prover = get_prover ctxt prover_name params goal facts
val problem =
{comment = "", state = st', goal = goal, subgoal = i,
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Oct 31 23:51:54 2014 +0100
@@ -171,7 +171,7 @@
let
val params = []
val res = Refute.refute_term (Proof_Context.init_global thy) params [] t
- val _ = Output.urgent_message ("Refute: " ^ res)
+ val _ = writeln ("Refute: " ^ res)
in
(rpair []) (case res of
"genuine" => GenuineCex
@@ -194,7 +194,7 @@
val state = Proof.init ctxt
val (res, _) = Nitpick.pick_nits_in_term state
(Nitpick_Commands.default_params thy []) Nitpick.Normal 1 1 1 [] [] [] t
- val _ = Output.urgent_message ("Nitpick: " ^ res)
+ val _ = writeln ("Nitpick: " ^ res)
in
(rpair []) (case res of
"genuine" => GenuineCex
@@ -343,21 +343,21 @@
(*
fun unsafe_invoke_mtd thy (mtd_name, invoke_mtd) t =
let
- val _ = Output.urgent_message ("Invoking " ^ mtd_name)
+ val _ = writeln ("Invoking " ^ mtd_name)
val ((res, (timing, reports)), time) = cpu_time "total time" (fn () => invoke_mtd thy t
handle ERROR s => (tracing s; (Error, ([], NONE))))
- val _ = Output.urgent_message (" Done")
+ val _ = writeln (" Done")
in (res, (time :: timing, reports)) end
*)
fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t =
let
- val _ = Output.urgent_message ("Invoking " ^ mtd_name)
+ val _ = writeln ("Invoking " ^ mtd_name)
val (res, timing) = elapsed_time "total time"
(fn () => case try (invoke_mtd thy) t of
SOME (res, _) => res
- | NONE => (Output.urgent_message ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
+ | NONE => (writeln ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
Error))
- val _ = Output.urgent_message (" Done")
+ val _ = writeln (" Done")
in (res, [timing]) end
(* creating entries *)
@@ -387,7 +387,7 @@
val mutants =
if exec then
let
- val _ = Output.urgent_message ("BEFORE PARTITION OF " ^
+ val _ = writeln ("BEFORE PARTITION OF " ^
string_of_int (length mutants) ^ " MUTANTS")
val (execs, noexecs) = List.partition (is_executable_term thy) (take_random (20 * max_mutants) mutants)
val _ = tracing ("AFTER PARTITION (" ^ string_of_int (length execs) ^
@@ -404,7 +404,7 @@
|> filter (is_some o try (Thm.cterm_of thy))
|> filter (is_some o try (Syntax.check_term (Proof_Context.init_global thy)))
|> take_random max_mutants
- val _ = map (fn t => Output.urgent_message ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
+ val _ = map (fn t => writeln ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
in
create_entry thy thm exec mutants mtds
end
@@ -458,7 +458,7 @@
(* theory -> mtd list -> thm list -> string -> unit *)
fun mutate_theorems_and_write_report thy (num_mutations, max_mutants) mtds thms file_name =
let
- val _ = Output.urgent_message "Starting Mutabelle..."
+ val _ = writeln "Starting Mutabelle..."
val ctxt = Proof_Context.init_global thy
val path = Path.explode file_name
(* for normal report: *)
--- a/src/HOL/ROOT Fri Oct 31 17:01:54 2014 +0000
+++ b/src/HOL/ROOT Fri Oct 31 23:51:54 2014 +0100
@@ -600,7 +600,6 @@
Simps_Case_Conv_Examples
ML
SAT_Examples
- Nominal2_Dummy
SOS
SOS_Cert
theories [skip_proofs = false]
@@ -759,7 +758,7 @@
Misc_Datatype
Misc_Primcorec
Misc_Primrec
- theories [condition = ISABELLE_FULL_TEST, timing]
+ theories [condition = ISABELLE_FULL_TEST]
Brackin
IsaFoR
Misc_N2M
@@ -1099,6 +1098,6 @@
Some benchmark on large record.
*}
options [document = false]
- theories [condition = ISABELLE_FULL_TEST, timing]
+ theories [condition = ISABELLE_FULL_TEST]
Record_Benchmark
--- a/src/HOL/TPTP/atp_problem_import.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/HOL/TPTP/atp_problem_import.ML Fri Oct 31 23:51:54 2014 +0100
@@ -117,7 +117,7 @@
if falsify then "CounterSatisfiable" else "Satisfiable"
else
"Unknown")
- |> Output.urgent_message
+ |> writeln
val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy snd file_name
val params =
[("maxtime", string_of_int timeout),
@@ -135,7 +135,7 @@
fun SOLVE_TIMEOUT seconds name tac st =
let
- val _ = Output.urgent_message ("running " ^ name ^ " for " ^ string_of_int seconds ^ " s")
+ val _ = writeln ("running " ^ name ^ " for " ^ string_of_int seconds ^ " s")
val result =
TimeLimit.timeLimit (Time.fromSeconds seconds) (fn () => SINGLE (SOLVE tac) st) ()
handle
@@ -143,8 +143,8 @@
| ERROR _ => NONE
in
(case result of
- NONE => (Output.urgent_message ("FAILURE: " ^ name); Seq.empty)
- | SOME st' => (Output.urgent_message ("SUCCESS: " ^ name); Seq.single st'))
+ NONE => (writeln ("FAILURE: " ^ name); Seq.empty)
+ | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st'))
end
fun nitpick_finite_oracle_tac ctxt timeout i th =
@@ -264,7 +264,7 @@
Logic.list_implies (rev defs @ rev nondefs, case conjs of conj :: _ => conj | [] => @{prop False})
fun print_szs_of_success conjs success =
- Output.urgent_message ("% SZS status " ^
+ writeln ("% SZS status " ^
(if success then
if null conjs then "Unsatisfiable" else "Theorem"
else
--- a/src/HOL/Tools/Nitpick/nitpick.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Oct 31 23:51:54 2014 +0100
@@ -241,11 +241,11 @@
o Pretty.mark Markup.information
else
print o Pretty.string_of
- val pprint_a = pprint Output.urgent_message
- fun pprint_nt f = () |> is_mode_nt mode ? pprint Output.urgent_message o f
- fun pprint_v f = () |> verbose ? pprint Output.urgent_message o f
+ val pprint_a = pprint writeln
+ fun pprint_nt f = () |> is_mode_nt mode ? pprint writeln o f
+ fun pprint_v f = () |> verbose ? pprint writeln o f
fun pprint_d f = () |> debug ? pprint tracing o f
- val print = pprint Output.urgent_message o curry Pretty.blk 0 o pstrs
+ val print = pprint writeln o curry Pretty.blk 0 o pstrs
fun print_t f = () |> mode = TPTP ? print o f
(*
val print_g = pprint tracing o Pretty.str
@@ -1015,8 +1015,8 @@
fun pick_nits_in_term state (params as {timeout, expect, ...}) mode i n step
subst def_assm_ts nondef_assm_ts orig_t =
let
- val print_nt = if is_mode_nt mode then Output.urgent_message else K ()
- val print_t = if mode = TPTP then Output.urgent_message else K ()
+ val print_nt = if is_mode_nt mode then writeln else K ()
+ val print_t = if mode = TPTP then writeln else K ()
in
if getenv "KODKODI" = "" then
(* The "expect" argument is deliberately ignored if Kodkodi is missing so
@@ -1068,7 +1068,7 @@
val t = state |> Proof.raw_goal |> #goal |> prop_of
in
case Logic.count_prems t of
- 0 => (Output.urgent_message "No subgoal!"; (noneN, state))
+ 0 => (writeln "No subgoal!"; (noneN, state))
| n =>
let
val t = Logic.goal_params t i |> fst
--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML Fri Oct 31 23:51:54 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/Nitpick/nitpick_hol.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Oct 31 23:51:54 2014 +0100
@@ -2140,8 +2140,7 @@
map (wf_constraint_for_triple rel) triples
|> foldr1 s_conj |> HOLogic.mk_Trueprop
val _ = if debug then
- Output.urgent_message ("Wellfoundedness goal: " ^
- Syntax.string_of_term ctxt prop ^ ".")
+ writeln ("Wellfoundedness goal: " ^ Syntax.string_of_term ctxt prop ^ ".")
else
()
in
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Oct 31 23:51:54 2014 +0100
@@ -1059,7 +1059,7 @@
if debug then
(if negate then "Genuineness" else "Spuriousness") ^ " goal: " ^
Syntax.string_of_term ctxt prop ^ "."
- |> Output.urgent_message
+ |> writeln
else
()
val goal = prop |> cterm_of thy |> Goal.init
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Oct 31 23:51:54 2014 +0100
@@ -360,7 +360,7 @@
fun try_upto_depth ctxt f =
let
val max_depth = Config.get ctxt Quickcheck.depth
- fun message s = if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message s
+ fun message s = if Config.get ctxt Quickcheck.quiet then () else writeln s
fun try' i =
if i <= max_depth then
let
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Oct 31 23:51:54 2014 +0100
@@ -221,8 +221,8 @@
fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code_modules, _) =
let
val ((is_genuine, counterexample_of), (get, put, put_ml)) = cookie
- fun message s = if quiet then () else Output.urgent_message s
- fun verbose_message s = if not quiet andalso verbose then Output.urgent_message s else ()
+ fun message s = if quiet then () else writeln s
+ fun verbose_message s = if not quiet andalso verbose then writeln s else ()
val current_size = Unsynchronized.ref 0
val current_result = Unsynchronized.ref Quickcheck.empty_result
val tmp_prefix = "Quickcheck_Narrowing"
@@ -511,7 +511,7 @@
(maps (map snd) correct_inst_goals) []
end
else
- (if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message
+ (if Config.get ctxt Quickcheck.quiet then () else writeln
("Environment variable ISABELLE_GHC is not set. To use narrowing-based quickcheck, please set "
^ "this variable to your GHC Haskell compiler in your settings file. "
^ "To deactivate narrowing-based quickcheck, set quickcheck_narrowing_active to false.");
--- a/src/HOL/Tools/Sledgehammer/async_manager.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/HOL/Tools/Sledgehammer/async_manager.ML Fri Oct 31 23:51:54 2014 +0100
@@ -106,7 +106,7 @@
tool ^ ": " ^
implode_message (workers |> sort_distinct string_ord, work)
|> break_into_chunks
- |> List.app Output.urgent_message)
+ |> List.app writeln)
fun check_thread_manager () = Synchronized.change global_state
(fn state as {manager, timeout_heap, active, canceling, messages, store} =>
@@ -178,7 +178,7 @@
val state' = make_state manager timeout_heap [] (killing @ canceling) messages store
val _ =
if null killing then ()
- else Output.urgent_message ("Interrupted active " ^ das_wort_worker ^ "s.")
+ else writeln ("Interrupted active " ^ das_wort_worker ^ "s.")
in state' end)
fun str_of_time time = string_of_int (Time.toSeconds time) ^ " s"
@@ -210,7 +210,7 @@
case map_filter canceling_info canceling of
[] => []
| ss => "Interrupting " ^ das_wort_worker ^ "s" :: ss
- in Output.urgent_message (space_implode "\n\n" (running @ interrupting)) end
+ in writeln (space_implode "\n\n" (running @ interrupting)) end
fun thread_messages tool das_wort_worker opt_limit =
let
@@ -222,6 +222,6 @@
(if length tool_store <= limit then ":"
else " (" ^ string_of_int limit ^ " displayed):")
val ss = tool_store |> chop limit |> #1 |> map (op ^ o snd)
- in List.app Output.urgent_message (header :: maps break_into_chunks ss) end
+ in List.app writeln (header :: maps break_into_chunks ss) end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 31 23:51:54 2014 +0100
@@ -137,7 +137,7 @@
|> commas
|> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
" proof (of " ^ string_of_int (length facts) ^ "): ") "."
- |> Output.urgent_message
+ |> writeln
fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) =
let
@@ -230,7 +230,7 @@
else
outcome
|> Async_Manager.break_into_chunks
- |> List.app Output.urgent_message
+ |> List.app writeln
in (outcome_code, state) end
else
(Async_Manager.thread SledgehammerN birth_time death_time
@@ -259,12 +259,12 @@
else
(case subgoal_count state of
0 =>
- ((if blocking then error else Output.urgent_message) "No subgoal!"; (false, (noneN, state)))
+ ((if blocking then error else writeln) "No subgoal!"; (false, (noneN, state)))
| n =>
let
val _ = Proof.assert_backward state
val print =
- if mode = Normal andalso is_none output_result then Output.urgent_message else K ()
+ if mode = Normal andalso is_none output_result then writeln else K ()
val ctxt = Proof.context_of state
val {facts = chained, goal, ...} = Proof.goal state
val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Oct 31 23:51:54 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/Sledgehammer/sledgehammer_isar.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Oct 31 23:51:54 2014 +0100
@@ -150,7 +150,7 @@
fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
(one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) =
let
- val _ = if debug then Output.urgent_message "Constructing Isar proof..." else ()
+ val _ = if debug then writeln "Constructing Isar proof..." else ()
fun generate_proof_text () =
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Oct 31 23:51:54 2014 +0100
@@ -1016,7 +1016,7 @@
val num_isar_deps = length isar_deps
in
if verbose andalso auto_level = 0 then
- Output.urgent_message ("MaSh: " ^ quote prover ^ " on " ^ quote name ^ " with " ^
+ writeln ("MaSh: " ^ quote prover ^ " on " ^ quote name ^ " with " ^
string_of_int num_isar_deps ^ " + " ^ string_of_int (length facts - num_isar_deps) ^
" facts.")
else
@@ -1025,7 +1025,7 @@
{outcome = NONE, used_facts, ...} =>
(if verbose andalso auto_level = 0 then
let val num_facts = length used_facts in
- Output.urgent_message ("Found proof with " ^ string_of_int num_facts ^ " fact" ^
+ writeln ("Found proof with " ^ string_of_int num_facts ^ " fact" ^
plural_s num_facts ^ ".")
end
else
@@ -1212,7 +1212,7 @@
|> pairself (map fact_of_raw_fact)
end
-fun mash_unlearn () = (clear_state (); Output.urgent_message "Reset MaSh.")
+fun mash_unlearn () = (clear_state (); writeln "Reset MaSh.")
fun learn_wrt_access_graph ctxt (name, parents, feats, deps)
(accum as (access_G, (fact_xtab, feat_xtab))) =
@@ -1361,11 +1361,11 @@
end
fun commit last learns relearns flops =
- (if debug andalso auto_level = 0 then Output.urgent_message "Committing..." else ();
+ (if debug andalso auto_level = 0 then writeln "Committing..." else ();
map_state ctxt (do_commit (rev learns) relearns flops);
if not last andalso auto_level = 0 then
let val num_proofs = length learns + length relearns in
- Output.urgent_message ("Learned " ^ string_of_int num_proofs ^ " " ^
+ writeln ("Learned " ^ string_of_int num_proofs ^ " " ^
(if run_prover then "automatic" else "Isar") ^ " proof" ^
plural_s num_proofs ^ " in the last " ^ string_of_time commit_timeout ^ ".")
end
@@ -1474,18 +1474,18 @@
fun learn auto_level run_prover =
mash_learn_facts ctxt params prover auto_level run_prover one_year facts
- |> Output.urgent_message
+ |> writeln
in
if run_prover then
- (Output.urgent_message ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
+ (writeln ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
plural_s num_facts ^ " for automatic proofs (" ^ quote prover ^ " timeout: " ^
string_of_time timeout ^ ").\n\nCollecting Isar proofs first...");
learn 1 false;
- Output.urgent_message "Now collecting automatic proofs. This may take several hours. You \
+ writeln "Now collecting automatic proofs. This may take several hours. You \
\can safely stop the learning process at any point.";
learn 0 true)
else
- (Output.urgent_message ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
+ (writeln ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
plural_s num_facts ^ " for Isar proofs...");
learn 0 false)
end
@@ -1522,7 +1522,7 @@
Time.toSeconds timeout >= min_secs_for_learning then
let val timeout = time_mult learn_timeout_slack timeout in
(if verbose then
- Output.urgent_message ("Started MaShing through " ^
+ writeln ("Started MaShing through " ^
(if exact then "" else "at least ") ^ string_of_int min_num_facts_to_learn ^
" fact" ^ plural_s min_num_facts_to_learn ^ " in the background.")
else
@@ -1545,7 +1545,7 @@
| num_facts_to_learn =>
if num_facts_to_learn <= max_facts_to_learn_before_query then
mash_learn_facts ctxt params prover 2 false timeout facts
- |> (fn "" => () | s => Output.urgent_message (MaShN ^ ": " ^ s))
+ |> (fn "" => () | s => writeln (MaShN ^ ": " ^ s))
else
maybe_launch_thread true num_facts_to_learn)
else
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Oct 31 23:51:54 2014 +0100
@@ -198,7 +198,7 @@
sort_strings (supported_atps thy) @ sort_strings (SMT_Config.available_solvers_of ctxt)
|> List.partition (String.isPrefix remote_prefix)
in
- Output.urgent_message ("Supported provers: " ^ commas (local_provers @ remote_provers) ^ ".")
+ writeln ("Supported provers: " ^ commas (local_provers @ remote_provers) ^ ".")
end
fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Oct 31 23:51:54 2014 +0100
@@ -250,7 +250,7 @@
quote name ^ " slice #" ^ string_of_int (slice + 1) ^
" with " ^ string_of_int num_facts ^ " fact" ^
plural_s num_facts ^ " for " ^ string_of_time slice_timeout ^ "..."
- |> Output.urgent_message
+ |> writeln
else
()
val readable_names = not (Config.get ctxt atp_full_names)
@@ -370,7 +370,7 @@
(used_facts, preferred_methss,
fn preplay =>
let
- val _ = if verbose then Output.urgent_message "Generating proof text..." else ()
+ val _ = if verbose then writeln "Generating proof text..." else ()
fun isar_params () =
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Oct 31 23:51:54 2014 +0100
@@ -76,7 +76,7 @@
(if n > 0 then ": " ^ (names |> map fst |> sort string_ord |> space_implode " ") else "")
end
-fun print silent f = if silent then () else Output.urgent_message (f ())
+fun print silent f = if silent then () else writeln (f ())
fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Fri Oct 31 23:51:54 2014 +0100
@@ -113,7 +113,7 @@
if debug then
quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^
" fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout
- |> Output.urgent_message
+ |> writeln
else
()
val birth = Timer.checkRealTimer timer
@@ -163,7 +163,7 @@
string_of_atp_failure (failure_of_smt_failure (the outcome)) ^
" Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
"..."
- |> Output.urgent_message
+ |> writeln
else
()
in
@@ -204,7 +204,7 @@
(preferred_methss,
fn preplay =>
let
- val _ = if verbose then Output.urgent_message "Generating proof text..." else ()
+ val _ = if verbose then writeln "Generating proof text..." else ()
fun isar_params () =
(verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (),
--- a/src/HOL/Tools/try0.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/HOL/Tools/try0.ML Fri Oct 31 23:51:54 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 =
@@ -131,12 +124,12 @@
if mode = Normal then
"Trying " ^ space_implode " " (Try.serial_commas "and" (map (quote o fst) named_methods)) ^
"..."
- |> Output.urgent_message
+ |> writeln
else
();
(case par_map (fn f => f mode timeout_opt quad st) apply_methods of
[] =>
- (if mode = Normal then Output.urgent_message "No proof found." else (); (false, (noneN, st)))
+ (if mode = Normal then writeln "No proof found." else (); (false, (noneN, st)))
| xs as (name, command, _) :: _ =>
let
val xs = xs |> map (fn (name, _, n) => (n, name))
@@ -159,7 +152,7 @@
|> (if mode = Auto_Try then
Proof.goal_message (fn () => Pretty.markup Markup.information [Pretty.str message])
else
- tap (fn _ => Output.urgent_message message))))
+ tap (fn _ => writeln message))))
end)
end;
--- a/src/HOL/ex/Nominal2_Dummy.thy Fri Oct 31 17:01:54 2014 +0000
+++ /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/antiquote.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/General/antiquote.ML Fri Oct 31 23:51:54 2014 +0100
@@ -49,12 +49,12 @@
val scan_txt =
Scan.repeat1 ($$$ "@" --| Scan.ahead (~$$ "{") ||
- Scan.many1 (fn (s, _) => s <> "@" andalso Symbol.is_regular s)) >> flat;
+ Scan.many1 (fn (s, _) => s <> "@" andalso Symbol.not_eof s)) >> flat;
val scan_antiq_body =
Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >> #2 ||
- Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
+ Scan.one (fn (s, _) => s <> "}" andalso Symbol.not_eof s) >> single;
in
--- a/src/Pure/General/output.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/General/output.ML Fri Oct 31 23:51:54 2014 +0100
@@ -26,11 +26,9 @@
val physical_writeln: output -> unit
exception Protocol_Message of Properties.T
val writelns: string list -> unit
- val urgent_message: string -> unit
val error_message': serial * string -> unit
val error_message: string -> unit
val system_message: string -> unit
- val prompt: string -> unit
val status: string -> unit
val report: string list -> unit
val result: Properties.T -> string list -> unit
@@ -42,12 +40,10 @@
sig
include OUTPUT
val writeln_fn: (output list -> unit) Unsynchronized.ref
- val urgent_message_fn: (output list -> unit) Unsynchronized.ref
val tracing_fn: (output list -> unit) Unsynchronized.ref
val warning_fn: (output list -> unit) Unsynchronized.ref
val error_message_fn: (serial * output list -> unit) Unsynchronized.ref
val system_message_fn: (output list -> unit) Unsynchronized.ref
- val prompt_fn: (output -> unit) Unsynchronized.ref
val status_fn: (output list -> unit) Unsynchronized.ref
val report_fn: (output list -> unit) Unsynchronized.ref
val result_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
@@ -98,13 +94,11 @@
exception Protocol_Message of Properties.T;
val writeln_fn = Unsynchronized.ref (physical_writeln o implode);
-val urgent_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss); (*Proof General legacy*)
val tracing_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### " o implode);
val error_message_fn =
Unsynchronized.ref (fn (_: serial, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
val system_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
-val prompt_fn = Unsynchronized.ref physical_stdout; (*Proof General legacy*)
val status_fn = Unsynchronized.ref (fn _: output list => ());
val report_fn = Unsynchronized.ref (fn _: output list => ());
val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output list => ());
@@ -113,13 +107,11 @@
fun writelns ss = ! writeln_fn (map output ss);
fun writeln s = writelns [s];
-fun urgent_message s = ! urgent_message_fn [output s]; (*Proof General legacy*)
fun tracing s = ! tracing_fn [output s];
fun warning s = ! warning_fn [output s];
fun error_message' (i, s) = ! error_message_fn (i, [output s]);
fun error_message s = error_message' (serial (), s);
fun system_message s = ! system_message_fn [output s];
-fun prompt s = ! prompt_fn (output s);
fun status s = ! status_fn [output s];
fun report ss = ! report_fn (map output ss);
fun result props ss = ! result_fn props (map output ss);
--- a/src/Pure/General/position.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/General/position.ML Fri Oct 31 23:51:54 2014 +0100
@@ -90,7 +90,7 @@
fun advance_count "\n" (i: int, j: int, k: int) =
(if_valid i (i + 1), if_valid j (j + 1), k)
| advance_count s (i, j, k) =
- if Symbol.is_regular s then (i, if_valid j (j + 1), k)
+ if Symbol.not_eof s then (i, if_valid j (j + 1), k)
else (i, j, k);
fun invalid_count (i, j, _: int) =
--- a/src/Pure/General/scan.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/General/scan.ML Fri Oct 31 23:51:54 2014 +0100
@@ -38,7 +38,6 @@
signature SCAN =
sig
include BASIC_SCAN
- val prompt: string -> ('a -> 'b) -> 'a -> 'b
val permissive: ('a -> 'b) -> 'a -> 'b
val error: ('a -> 'b) -> 'a -> 'b
val catch: ('a -> 'b) -> 'a -> 'b (*exception Fail*)
@@ -76,8 +75,8 @@
-> 'b * 'a list -> 'c * ('d * 'a list)
val finite: 'a stopper -> ('a list -> 'b * 'a list) -> 'a list -> 'b * 'a list
val read: 'a stopper -> ('a list -> 'b * 'a list) -> 'a list -> 'b option
- val drain: string -> (string -> 'a -> 'b list * 'a) -> 'b stopper ->
- ('c * 'b list -> 'd * ('e * 'b list)) -> ('c * 'b list) * 'a -> ('d * ('e * 'b list)) * 'a
+ val drain: ('a -> 'b list * 'a) -> 'b stopper -> ('c * 'b list -> 'd * ('e * 'b list)) ->
+ ('c * 'b list) * 'a -> ('d * ('e * 'b list)) * 'a
type lexicon
val is_literal: lexicon -> string list -> bool
val literal: lexicon -> (string * 'a) list -> (string * 'a) list * (string * 'a) list
@@ -98,14 +97,13 @@
type message = unit -> string;
-exception MORE of string option; (*need more input (prompt)*)
-exception FAIL of message option; (*try alternatives (reason of failure)*)
-exception ABORT of message; (*dead end*)
+exception MORE of unit; (*need more input*)
+exception FAIL of message option; (*try alternatives (reason of failure)*)
+exception ABORT of message; (*dead end*)
fun !! err scan xs = scan xs handle FAIL msg => raise ABORT (err (xs, msg));
-fun permissive scan xs = scan xs handle MORE _ => raise FAIL NONE | ABORT _ => raise FAIL NONE;
-fun strict scan xs = scan xs handle MORE _ => raise FAIL NONE;
-fun prompt str scan xs = scan xs handle MORE NONE => raise MORE (SOME str);
+fun permissive scan xs = scan xs handle MORE () => raise FAIL NONE | ABORT _ => raise FAIL NONE;
+fun strict scan xs = scan xs handle MORE () => raise FAIL NONE;
fun error scan xs = scan xs handle ABORT msg => Library.error (msg ());
fun catch scan xs = scan xs
@@ -140,11 +138,11 @@
fun fail_with msg_of xs = raise FAIL (SOME (msg_of xs));
fun succeed y xs = (y, xs);
-fun some _ [] = raise MORE NONE
+fun some _ [] = raise MORE ()
| some f (x :: xs) =
(case f x of SOME y => (y, xs) | _ => raise FAIL NONE);
-fun one _ [] = raise MORE NONE
+fun one _ [] = raise MORE ()
| one pred (x :: xs) =
if pred x then (x, xs) else raise FAIL NONE;
@@ -154,14 +152,14 @@
fun this ys xs =
let
fun drop_prefix [] xs = xs
- | drop_prefix (_ :: _) [] = raise MORE NONE
+ | drop_prefix (_ :: _) [] = raise MORE ()
| drop_prefix (y :: ys) (x :: xs) =
if (y: string) = x then drop_prefix ys xs else raise FAIL NONE;
in (ys, drop_prefix ys xs) end;
fun this_string s = this (raw_explode s) >> K s; (*primitive string -- no symbols here!*)
-fun many _ [] = raise MORE NONE
+fun many _ [] = raise MORE ()
| many pred (lst as x :: xs) =
if pred x then apfst (cons x) (many pred xs)
else ([], lst);
@@ -265,11 +263,11 @@
(* infinite scans -- draining state-based source *)
-fun drain def_prompt get stopper scan ((state, xs), src) =
- (scan (state, xs), src) handle MORE prompt =>
- (case get (the_default def_prompt prompt) src of
+fun drain get stopper scan ((state, xs), src) =
+ (scan (state, xs), src) handle MORE () =>
+ (case get src of
([], _) => (finite' stopper scan (state, xs), src)
- | (xs', src') => drain def_prompt get stopper scan ((state, xs @ xs'), src'));
+ | (xs', src') => drain get stopper scan ((state, xs @ xs'), src'));
@@ -292,7 +290,8 @@
let
fun finish (SOME (res, rest)) = (rev res, rest)
| finish NONE = raise FAIL NONE;
- fun scan _ res (Lexicon tab) [] = if Symtab.is_empty tab then finish res else raise MORE NONE
+ fun scan _ res (Lexicon tab) [] =
+ if Symtab.is_empty tab then finish res else raise MORE ()
| scan path res (Lexicon tab) (c :: cs) =
(case Symtab.lookup tab (fst c) of
SOME (tip, lex) =>
--- a/src/Pure/General/secure.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/General/secure.ML Fri Oct 31 23:51:54 2014 +0100
@@ -13,8 +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;
structure Secure: SECURE =
@@ -33,8 +31,6 @@
(** critical operations **)
-(* ML evaluation *)
-
fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode";
val raw_use_text = use_text;
@@ -46,15 +42,5 @@
fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp ML_Parse.global_context path pp);
-
-(* global evaluation *)
-
-val use_global = raw_use_text ML_Parse.global_context (0, "") false;
-
-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/General/source.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/General/source.ML Fri Oct 31 23:51:54 2014 +0100
@@ -7,8 +7,6 @@
signature SOURCE =
sig
type ('a, 'b) source
- val default_prompt: string
- val set_prompt: string -> ('a, 'b) source -> ('a, 'b) source
val get: ('a, 'b) source -> 'a list * ('a, 'b) source
val unget: 'a list * ('a, 'b) source -> ('a, 'b) source
val get_single: ('a, 'b) source -> ('a * ('a, 'b) source) option
@@ -19,7 +17,6 @@
val exhausted: ('a, 'b) source -> ('a, 'a list) source
val of_string: string -> (string, string list) source
val of_string_limited: int -> string -> (string, substring) source
- val tty: TextIO.instream -> (string, unit) source
val source': 'a -> 'b Scan.stopper -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
(bool * (string -> 'a * 'b list -> 'c list * ('a * 'b list))) option ->
('b, 'e) source -> ('c, 'a * ('b, 'e) source) source
@@ -38,37 +35,24 @@
Source of
{buffer: 'a list,
info: 'b,
- prompt: string,
- drain: string -> 'b -> 'a list * 'b};
-
-fun make_source buffer info prompt drain =
- Source {buffer = buffer, info = info, prompt = prompt, drain = drain};
-
+ drain: 'b -> 'a list * 'b};
-(* prompt *)
-
-val default_prompt = "> ";
-
-fun set_prompt prompt (Source {buffer, info, prompt = _, drain}) =
- make_source buffer info prompt drain;
+fun make_source buffer info drain =
+ Source {buffer = buffer, info = info, drain = drain};
(* get / unget *)
-fun get (Source {buffer = [], info, prompt, drain}) =
- let val (xs, info') = drain prompt info
- in (xs, make_source [] info' prompt drain) end
- | get (Source {buffer, info, prompt, drain}) =
- (buffer, make_source [] info prompt drain);
+fun get (Source {buffer = [], info, drain}) =
+ let val (xs, info') = drain info
+ in (xs, make_source [] info' drain) end
+ | get (Source {buffer, info, drain}) = (buffer, make_source [] info drain);
-fun unget (xs, Source {buffer, info, prompt, drain}) =
- make_source (xs @ buffer) info prompt drain;
+fun unget (xs, Source {buffer, info, drain}) = make_source (xs @ buffer) info drain;
(* variations on get *)
-fun get_prompt prompt src = get (set_prompt prompt src);
-
fun get_single src =
(case get src of
([], _) => NONE
@@ -82,16 +66,16 @@
(* (map)filter *)
-fun drain_map_filter f prompt src =
+fun drain_map_filter f src =
let
- val (xs, src') = get_prompt prompt src;
+ val (xs, src') = get src;
val xs' = map_filter f xs;
in
if null xs orelse not (null xs') then (xs', src')
- else drain_map_filter f prompt src'
+ else drain_map_filter f src'
end;
-fun map_filter f src = make_source [] src default_prompt (drain_map_filter f);
+fun map_filter f src = make_source [] src (drain_map_filter f);
fun filter pred = map_filter (fn x => if pred x then SOME x else NONE);
@@ -100,7 +84,7 @@
(* list source *)
-fun of_list xs = make_source [] xs default_prompt (fn _ => fn xs => (xs, []));
+fun of_list xs = make_source [] xs (fn xs => (xs, []));
fun exhausted src = of_list (exhaust src);
@@ -110,44 +94,23 @@
val of_string = of_list o raw_explode;
fun of_string_limited limit str =
- make_source [] (Substring.full str) default_prompt
- (fn _ => fn s =>
+ make_source [] (Substring.full str)
+ (fn s =>
let
val (s1, s2) = Substring.splitAt (s, Int.min (Substring.size s, limit));
val cs = map String.str (Substring.explode s1);
in (cs, s2) end);
-(* stream source *)
-
-fun slurp_input instream =
- let
- fun slurp () =
- (case TextIO.canInput (instream, 1) handle IO.Io _ => NONE of
- NONE => []
- | SOME 0 => []
- | SOME _ => TextIO.input instream :: slurp ());
- in maps raw_explode (slurp ()) end;
-
-fun tty in_stream = make_source [] () default_prompt (fn prompt => fn () =>
- let val input = slurp_input in_stream in
- if exists (fn c => c = "\n") input then (input, ())
- else
- (case (Output.prompt prompt; TextIO.inputLine in_stream) of
- SOME line => (input @ raw_explode line, ())
- | NONE => (input, ()))
- end);
-
-
(** cascade sources **)
(* state-based *)
-fun drain_source' stopper scan opt_recover prompt (state, src) =
+fun drain_source' stopper scan opt_recover (state, src) =
let
- val drain = Scan.drain prompt get_prompt stopper;
- val (xs, s) = get_prompt prompt src;
+ val drain = Scan.drain get stopper;
+ val (xs, s) = get src;
val inp = ((state, xs), s);
val ((ys, (state', xs')), src') =
if null xs then (([], (state, [])), s)
@@ -162,17 +125,16 @@
in (ys, (state', unget (xs', src'))) end;
fun source' init_state stopper scan recover src =
- make_source [] (init_state, src) default_prompt (drain_source' stopper scan recover);
+ make_source [] (init_state, src) (drain_source' stopper scan recover);
(* non state-based *)
-fun drain_source stopper scan opt_recover prompt =
+fun drain_source stopper scan opt_recover =
Scan.unlift (drain_source' stopper (Scan.lift scan)
- (Option.map (fn (int, r) => (int, Scan.lift o r)) opt_recover) prompt);
+ (Option.map (fn (int, r) => (int, Scan.lift o r)) opt_recover));
fun source stopper scan recover src =
- make_source [] src default_prompt (drain_source stopper scan recover);
-
+ make_source [] src (drain_source stopper scan recover);
end;
--- a/src/Pure/General/symbol.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/General/symbol.ML Fri Oct 31 23:51:54 2014 +0100
@@ -19,9 +19,6 @@
val is_eof: symbol -> bool
val not_eof: symbol -> bool
val stopper: symbol Scan.stopper
- val sync: symbol
- val is_sync: symbol -> bool
- val is_regular: symbol -> bool
val is_malformed: symbol -> bool
val malformed_msg: symbol -> string
val is_ascii: symbol -> bool
@@ -119,12 +116,6 @@
fun not_eof s = s <> eof;
val stopper = Scan.stopper (K eof) is_eof;
-(*Proof General legacy*)
-val sync = "\\<^sync>";
-fun is_sync s = s = sync;
-
-fun is_regular s = not_eof s andalso s <> sync;
-
fun is_malformed s =
String.isPrefix "\\<" s andalso not (String.isSuffix ">" s)
orelse s = "\\<>" orelse s = "\\<^>";
--- a/src/Pure/General/symbol_pos.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/General/symbol_pos.ML Fri Oct 31 23:51:54 2014 +0100
@@ -17,7 +17,6 @@
val is_eof: T -> bool
val stopper: T Scan.stopper
val !!! : Scan.message -> (T list -> 'a) -> T list -> 'a
- val change_prompt: ('a -> 'b) -> 'a -> 'b
val scan_pos: T list -> Position.T * T list
val scan_string_q: string -> T list -> (Position.T * (T list * Position.T)) * T list
val scan_string_qq: string -> T list -> (Position.T * (T list * Position.T)) * T list
@@ -88,8 +87,6 @@
(case msg of NONE => "" | SOME m => "\n" ^ m ());
in Scan.!! err scan end;
-fun change_prompt scan = Scan.prompt "# " scan;
-
fun $$ s = Scan.one (fn x => symbol x = s);
fun ~$$ s = Scan.one (fn x => symbol x <> s);
@@ -114,13 +111,13 @@
fun scan_str q err_prefix =
$$$ "\\" |-- !!! (fn () => err_prefix ^ "bad escape character in string")
($$$ q || $$$ "\\" || char_code) ||
- Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.is_regular s) >> single;
+ Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.not_eof s) >> single;
fun scan_strs q err_prefix =
Scan.ahead ($$ q) |--
!!! (fn () => err_prefix ^ "unclosed string literal")
((scan_pos --| $$$ q) --
- (change_prompt ((Scan.repeat (scan_str q err_prefix) >> flat) -- ($$$ q |-- scan_pos))));
+ ((Scan.repeat (scan_str q err_prefix) >> flat) -- ($$$ q |-- scan_pos)));
fun recover_strs q =
$$$ q @@@ (Scan.repeat (Scan.permissive (scan_str q "")) >> flat);
@@ -167,14 +164,14 @@
Scan.repeat1 (Scan.depend (fn (d: int) =>
$$ "\\<open>" >> pair (d + 1) ||
(if d > 0 then
- Scan.one (fn (s, _) => s <> "\\<close>" andalso Symbol.is_regular s) >> pair d ||
+ Scan.one (fn (s, _) => s <> "\\<close>" andalso Symbol.not_eof s) >> pair d ||
$$ "\\<close>" >> pair (d - 1)
else Scan.fail)));
fun scan_cartouche err_prefix =
Scan.ahead ($$ "\\<open>") |--
!!! (fn () => err_prefix ^ "unclosed text cartouche")
- (change_prompt (Scan.provide (fn d => d = 0) 0 scan_cartouche_depth));
+ (Scan.provide (fn d => d = 0) 0 scan_cartouche_depth);
val recover_cartouche = Scan.pass 0 scan_cartouche_depth;
@@ -201,23 +198,21 @@
Scan.depend (fn (d: int) => $$$ "(" @@@ $$$ "*" >> pair (d + 1)) ||
Scan.depend (fn 0 => Scan.fail | d => $$$ "*" @@@ $$$ ")" >> pair (d - 1)) ||
Scan.lift ($$$ "*" --| Scan.ahead (~$$$ ")")) ||
- Scan.lift (Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s)) >> single;
+ Scan.lift (Scan.one (fn (s, _) => s <> "*" andalso Symbol.not_eof s)) >> single;
val scan_cmts = Scan.pass 0 (Scan.repeat scan_cmt >> flat);
-val scan_body = change_prompt scan_cmts;
-
in
fun scan_comment err_prefix =
Scan.ahead ($$ "(" -- $$ "*") |--
!!! (fn () => err_prefix ^ "unclosed comment")
- ($$$ "(" @@@ $$$ "*" @@@ scan_body @@@ $$$ "*" @@@ $$$ ")");
+ ($$$ "(" @@@ $$$ "*" @@@ scan_cmts @@@ $$$ "*" @@@ $$$ ")");
fun scan_comment_body err_prefix =
Scan.ahead ($$ "(" -- $$ "*") |--
!!! (fn () => err_prefix ^ "unclosed comment")
- ($$ "(" |-- $$ "*" |-- scan_body --| $$ "*" --| $$ ")");
+ ($$ "(" |-- $$ "*" |-- scan_cmts --| $$ "*" --| $$ ")");
val recover_comment =
$$$ "(" @@@ $$$ "*" @@@ scan_cmts;
--- a/src/Pure/General/url.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/General/url.ML Fri Oct 31 23:51:54 2014 +0100
@@ -54,11 +54,11 @@
local
val scan_host =
- (Scan.many1 (fn s => s <> "/" andalso Symbol.is_regular s) >> implode) --|
+ (Scan.many1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --|
Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
-val scan_path = Scan.many Symbol.is_regular >> (Path.explode o implode);
-val scan_path_root = Scan.many Symbol.is_regular >> (Path.explode o implode o cons "/");
+val scan_path = Scan.many Symbol.not_eof >> (Path.explode o implode);
+val scan_path_root = Scan.many Symbol.not_eof >> (Path.explode o implode o cons "/");
val scan_url =
Scan.unless (Scan.this_string "file:" ||
--- a/src/Pure/Isar/calculation.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/Isar/calculation.ML Fri Oct 31 23:51:54 2014 +0100
@@ -120,7 +120,7 @@
if int then
Proof_Context.pretty_fact ctxt'
(Proof_Context.full_name ctxt' (Binding.name calculationN), calc)
- |> Pretty.string_of |> Output.urgent_message
+ |> Pretty.string_of |> writeln
else ();
in state' |> final ? (put_calculation NONE #> Proof.chain_facts calc) end;
--- a/src/Pure/Isar/isar_syn.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/Isar/isar_syn.ML Fri Oct 31 23:51:54 2014 +0100
@@ -734,23 +734,6 @@
-(** nested commands **)
-
-val props_text =
- Scan.optional Parse.properties [] -- Parse.position Parse.string
- >> (fn (props, (str, pos)) =>
- (Position.of_properties (Position.default_properties pos props), str));
-
-val _ =
- Outer_Syntax.improper_command @{command_spec "Isabelle.command"} "evaluate nested Isabelle command"
- (props_text :|-- (fn (pos, str) =>
- (case Outer_Syntax.parse (Outer_Syntax.get_syntax ()) pos str of
- [tr] => Scan.succeed (K tr)
- | _ => Scan.fail_with (K (fn () => "exactly one command expected")))
- handle ERROR msg => Scan.fail_with (K (fn () => msg))));
-
-
-
(** diagnostic commands (for interactive mode only) **)
val opt_modes =
@@ -758,11 +741,6 @@
val opt_bang = Scan.optional (@{keyword "!"} >> K true) false;
-val _ = (*Proof General legacy*)
- Outer_Syntax.improper_command @{command_spec "pretty_setmargin"}
- "change default margin for pretty printing"
- (Parse.nat >> (fn n => Toplevel.imperative (fn () => Pretty.margin_default := n)));
-
val _ =
Outer_Syntax.improper_command @{command_spec "help"}
"retrieve outer syntax commands according to name patterns"
@@ -890,13 +868,6 @@
(Scan.succeed Isar_Cmd.locale_deps);
val _ =
- Outer_Syntax.improper_command @{command_spec "print_binds"}
- "print term bindings of proof context -- Proof General legacy"
- (Scan.succeed (Toplevel.unknown_context o
- Toplevel.keep
- (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
-
-val _ =
Outer_Syntax.improper_command @{command_spec "print_term_bindings"}
"print term bindings of proof context"
(Scan.succeed (Toplevel.unknown_context o
@@ -948,110 +919,20 @@
(Scan.succeed (Toplevel.unknown_theory o
Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
-
-
-(** system commands (for interactive mode only) **)
-
-val _ =
- Outer_Syntax.improper_command @{command_spec "use_thy"} "use theory file"
- (Parse.position Parse.name >>
- (fn name => Toplevel.imperative (fn () => Thy_Info.use_thy name)));
-
-val _ =
- Outer_Syntax.improper_command @{command_spec "remove_thy"} "remove theory from loader database"
- (Parse.name >> (fn name => Toplevel.imperative (fn () => Thy_Info.remove_thy name)));
-
-val _ =
- Outer_Syntax.improper_command @{command_spec "kill_thy"}
- "kill theory -- try to remove from loader database"
- (Parse.name >> (fn name => Toplevel.imperative (fn () => Thy_Info.kill_thy name)));
-
-val _ = (*partial Proof General legacy*)
- Outer_Syntax.improper_command @{command_spec "display_drafts"}
- "display raw source files with symbols"
- (Scan.repeat1 Parse.path >> (fn names =>
- Toplevel.imperative (fn () => ignore (Present.display_drafts (map Path.explode names)))));
-
val _ =
Outer_Syntax.improper_command @{command_spec "print_state"}
"print current proof state (if present)"
(opt_modes >> (fn modes => Toplevel.keep (Print_Mode.with_modes modes Toplevel.print_state)));
-val _ = (*Proof General legacy, e.g. for ProofGeneral-3.7.x*)
- Outer_Syntax.improper_command @{command_spec "pr"} "print current proof state (if present)"
- (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
- Toplevel.keep (fn state =>
- (if Isabelle_Process.is_active () then error "Illegal TTY command" else ();
- case limit of NONE => () | SOME n => Options.default_put_int @{system_option goals_limit} n;
- Toplevel.quiet := false;
- Print_Mode.with_modes modes Toplevel.print_state state))));
-
-val _ = (*Proof General legacy*)
- Outer_Syntax.improper_command @{command_spec "disable_pr"}
- "disable printing of toplevel state"
- (Scan.succeed (Toplevel.imperative (fn () => Toplevel.quiet := true)));
-
-val _ = (*Proof General legacy*)
- Outer_Syntax.improper_command @{command_spec "enable_pr"}
- "enable printing of toplevel state"
- (Scan.succeed (Toplevel.imperative (fn () => Toplevel.quiet := false)));
-
-val _ =
- Outer_Syntax.improper_command @{command_spec "commit"}
- "commit current session to ML session image"
- (Parse.opt_unit >> K (Toplevel.imperative Secure.commit));
-
-val _ =
- Outer_Syntax.improper_command @{command_spec "quit"} "quit Isabelle process"
- (Parse.opt_unit >> (K (Toplevel.imperative quit)));
-
-val _ =
- Outer_Syntax.improper_command @{command_spec "exit"} "exit Isar loop"
- (Scan.succeed
- (Toplevel.keep (fn state =>
- (Context.set_thread_data (try Toplevel.generic_theory_of state);
- raise Runtime.TERMINATE))));
-
val _ =
Outer_Syntax.improper_command @{command_spec "welcome"} "print welcome message"
(Scan.succeed (Toplevel.imperative (writeln o Session.welcome)));
-
-
-(** raw Isar read-eval-print loop **)
-
val _ =
- Outer_Syntax.improper_command @{command_spec "init_toplevel"} "init toplevel point-of-interest"
- (Scan.succeed (Toplevel.imperative Isar.init));
-
-val _ =
- Outer_Syntax.improper_command @{command_spec "linear_undo"} "undo commands"
- (Scan.optional Parse.nat 1 >>
- (fn n => Toplevel.imperative (fn () => Isar.linear_undo n)));
-
-val _ =
- Outer_Syntax.improper_command @{command_spec "undo"} "undo commands (skipping closed proofs)"
- (Scan.optional Parse.nat 1 >>
- (fn n => Toplevel.imperative (fn () => Isar.undo n)));
-
-val _ =
- Outer_Syntax.improper_command @{command_spec "undos_proof"}
- "undo commands (skipping closed proofs)"
- (Scan.optional Parse.nat 1 >> (fn n =>
- Toplevel.keep (fn state =>
- if Toplevel.is_proof state then (Isar.undo n; Isar.print ()) else raise Toplevel.UNDEF)));
-
-val _ =
- Outer_Syntax.improper_command @{command_spec "cannot_undo"}
- "partial undo -- Proof General legacy"
- (Parse.name >>
- (fn "end" => Toplevel.imperative (fn () => Isar.undo 1)
- | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
-
-val _ =
- Outer_Syntax.improper_command @{command_spec "kill"}
- "kill partial proof or theory development"
- (Scan.succeed (Toplevel.imperative Isar.kill));
+ Outer_Syntax.improper_command @{command_spec "display_drafts"}
+ "display raw source files with symbols"
+ (Scan.repeat1 Parse.path >> (fn names =>
+ Toplevel.imperative (fn () => ignore (Present.display_drafts (map Path.explode names)))));
--- a/src/Pure/Isar/keyword.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/Isar/keyword.ML Fri Oct 31 23:51:54 2014 +0100
@@ -9,7 +9,6 @@
type T
val kind_of: T -> string
val kind_files_of: T -> string * string list
- val control: T
val diag: T
val thy_begin: T
val thy_end: T
@@ -56,8 +55,6 @@
val dest: unit -> string list * string list
val define: string * T option -> unit
val is_diag: string -> bool
- val is_control: string -> bool
- val is_regular: string -> bool
val is_heading: string -> bool
val is_theory_begin: string -> bool
val is_theory_load: string -> bool
@@ -92,7 +89,6 @@
(* kinds *)
-val control = kind "control";
val diag = kind "diag";
val thy_begin = kind "thy_begin";
val thy_end = kind "thy_end";
@@ -124,7 +120,7 @@
val prf_script = kind "prf_script";
val kinds =
- [control, diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
+ [diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
thy_load, thy_decl, thy_decl_block, thy_goal, qed, qed_script, qed_block, qed_global,
prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open,
prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
@@ -238,8 +234,6 @@
end;
val is_diag = command_category [diag];
-val is_control = command_category [control];
-val is_regular = not o command_category [diag, control];
val is_heading =
command_category [thy_heading1, thy_heading2, thy_heading3, thy_heading4,
--- a/src/Pure/Isar/keyword.scala Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/Isar/keyword.scala Fri Oct 31 23:51:54 2014 +0100
@@ -12,7 +12,6 @@
/* kinds */
val MINOR = "minor"
- val CONTROL = "control"
val DIAG = "diag"
val THY_BEGIN = "thy_begin"
val THY_END = "thy_end"
@@ -46,7 +45,6 @@
/* categories */
val diag = Set(DIAG)
- val control = Set(CONTROL)
val heading = Set(THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
PRF_HEADING2, PRF_HEADING3, PRF_HEADING4)
--- a/src/Pure/Isar/outer_syntax.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/Isar/outer_syntax.ML Fri Oct 31 23:51:54 2014 +0100
@@ -35,8 +35,6 @@
val parse: (Scan.lexicon * Scan.lexicon) * outer_syntax ->
Position.T -> string -> Toplevel.transition list
val parse_spans: Token.T list -> Command_Span.span list
- type isar
- val isar: TextIO.instream -> bool -> isar
val side_comments: Token.T list -> Token.T list
val command_reports: outer_syntax -> Token.T -> Position.report_text list
val read_spans: outer_syntax -> Token.T list -> Toplevel.transition list
@@ -77,14 +75,12 @@
local
fun terminate false = Scan.succeed ()
- | terminate true =
- Parse.group (fn () => "end of input")
- (Scan.option Parse.sync -- Parse.semicolon >> K ());
+ | terminate true = Parse.group (fn () => "end of input") (Parse.semicolon >> K ());
fun body cmd (name, _) =
(case cmd name of
SOME (Command {int_only, parse, ...}) =>
- Parse.!!! (Scan.prompt (name ^ "# ") (Parse.tags |-- parse >> pair int_only))
+ Parse.!!! (Parse.tags |-- parse >> pair int_only)
| NONE =>
Scan.succeed (false, Toplevel.imperative (fn () =>
error ("Bad parser for outer syntax command " ^ quote name))));
@@ -93,7 +89,6 @@
fun parse_command do_terminate cmd =
Parse.semicolon >> K NONE ||
- Parse.sync >> K NONE ||
(Parse.position Parse.command :-- body cmd) --| terminate do_terminate
>> (fn ((name, pos), (int_only, f)) =>
SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
@@ -184,8 +179,6 @@
| missing => error ("Missing outer syntax command(s) " ^ commas_quote missing))
end;
-fun lookup_commands_dynamic () = lookup_commands (! global_outer_syntax);
-
fun command (spec, pos) comment parse =
add_command spec (new_command comment NONE false parse pos);
@@ -238,10 +231,8 @@
fun toplevel_source term do_recover cmd src =
let
- val no_terminator =
- Scan.unless Parse.semicolon (Scan.one (Token.not_sync andf Token.not_eof));
- fun recover int =
- (int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]);
+ val no_terminator = Scan.unless Parse.semicolon (Scan.one Token.not_eof);
+ fun recover int = (int, fn _ => Scan.repeat no_terminator >> K [NONE]);
in
src
|> Token.source_proper
@@ -303,24 +294,6 @@
end;
-(* interactive source of toplevel transformers *)
-
-type isar =
- (Toplevel.transition, (Toplevel.transition option,
- (Token.T, (Token.T option, (Token.T, (Token.T,
- (Symbol_Pos.T,
- Position.T * (Symbol.symbol, (Symbol.symbol, (string, unit) Source.source) Source.source)
- Source.source) Source.source) Source.source) Source.source)
- Source.source) Source.source) Source.source) Source.source;
-
-fun isar in_stream term : isar =
- Source.tty in_stream
- |> Symbol.source
- |> Source.map_filter (fn "\<^newline>" => SOME "\n" | s => SOME s) (*Proof General legacy*)
- |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none
- |> toplevel_source term (SOME true) lookup_commands_dynamic;
-
-
(* side-comments *)
fun cmts (t1 :: t2 :: toks) =
--- a/src/Pure/Isar/outer_syntax.scala Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/Isar/outer_syntax.scala Fri Oct 31 23:51:54 2014 +0100
@@ -129,7 +129,7 @@
val keywords1 = keywords + (name -> kind)
val lexicon1 = lexicon + name
val completion1 =
- if (Keyword.control(kind._1) || replace == Some("")) completion
+ if (replace == Some("")) completion
else completion + (name, replace getOrElse name)
new Outer_Syntax(keywords1, lexicon1, completion1, language_context, true)
}
--- a/src/Pure/Isar/parse.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/Isar/parse.ML Fri Oct 31 23:51:54 2014 +0100
@@ -32,7 +32,6 @@
val alt_string: string parser
val verbatim: string parser
val cartouche: string parser
- val sync: string parser
val eof: string parser
val command_name: string -> string parser
val keyword_with: (string -> bool) -> string parser
@@ -196,7 +195,6 @@
val alt_string = kind Token.AltString;
val verbatim = kind Token.Verbatim;
val cartouche = kind Token.Cartouche;
-val sync = kind Token.Sync;
val eof = kind Token.EOF;
fun command_name x =
--- a/src/Pure/Isar/runtime.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/Isar/runtime.ML Fri Oct 31 23:51:54 2014 +0100
@@ -172,7 +172,7 @@
(fn () =>
debugging NONE body () handle exn =>
if Exn.is_interrupt exn then ()
- else Output.urgent_message ("## INTERNAL ERROR ##\n" ^ exn_message exn),
+ else writeln ("## INTERNAL ERROR ##\n" ^ exn_message exn),
Simple_Thread.attributes interrupts);
end;
--- a/src/Pure/Isar/specification.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/Isar/specification.ML Fri Oct 31 23:51:54 2014 +0100
@@ -74,7 +74,6 @@
(thm list list -> local_theory -> local_theory) -> Attrib.binding ->
(xstring * Position.T) list -> Element.context list -> Element.statement ->
bool -> local_theory -> Proof.state
- val add_theorem_hook: (bool -> Proof.state -> Proof.state) -> Context.generic -> Context.generic
end;
structure Specification: SPECIFICATION =
@@ -372,14 +371,6 @@
#2 #> pair ths);
in ((more_atts, prems, stmt, SOME facts), goal_ctxt) end);
-structure Theorem_Hook = Generic_Data
-(
- type T = ((bool -> Proof.state -> Proof.state) * stamp) list;
- val empty = [];
- val extend = I;
- fun merge data : T = Library.merge (eq_snd op =) data;
-);
-
fun gen_theorem schematic bundle_includes prep_att prep_stmt
kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int lthy =
let
@@ -419,7 +410,6 @@
|> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
|> tap (fn state => not schematic andalso Proof.schematic_goal state andalso
error "Illegal schematic goal statement")
- |> fold_rev (fn (f, _) => f int) (Theorem_Hook.get (Context.Proof goal_ctxt))
end;
in
@@ -434,8 +424,6 @@
val schematic_theorem_cmd =
gen_theorem true Bundle.includes_cmd Attrib.check_src Expression.read_statement;
-fun add_theorem_hook f = Theorem_Hook.map (cons (f, stamp ()));
-
end;
end;
--- a/src/Pure/Isar/token.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/Isar/token.ML Fri Oct 31 23:51:54 2014 +0100
@@ -9,7 +9,7 @@
datatype kind =
Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
Nat | Float | String | AltString | Verbatim | Cartouche | Space | Comment | InternalValue |
- Error of string | Sync | EOF
+ Error of string | EOF
val str_of_kind: kind -> string
type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
type T
@@ -35,7 +35,6 @@
val eof: T
val is_eof: T -> bool
val not_eof: T -> bool
- val not_sync: T -> bool
val stopper: T Scan.stopper
val kind_of: T -> kind
val is_kind: kind -> T -> bool
@@ -104,7 +103,7 @@
datatype kind =
Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
Nat | Float | String | AltString | Verbatim | Cartouche | Space | Comment | InternalValue |
- Error of string | Sync | EOF;
+ Error of string | EOF;
val str_of_kind =
fn Command => "command"
@@ -125,7 +124,6 @@
| Comment => "comment text"
| InternalValue => "internal value"
| Error _ => "bad input"
- | Sync => "sync marker"
| EOF => "end-of-input";
val delimited_kind = member (op =) [String, AltString, Verbatim, Cartouche, Comment];
@@ -201,7 +199,7 @@
in (Src {name = (name, pos), args = args, output_info = SOME (kind, markup)}, x) end;
-(* control tokens *)
+(* stopper *)
fun mk_eof pos = Token (("", (pos, Position.none)), (EOF, ""), Slot);
val eof = mk_eof Position.none;
@@ -211,9 +209,6 @@
val not_eof = not o is_eof;
-fun not_sync (Token (_, (Sync, _), _)) = false
- | not_sync _ = true;
-
val stopper =
Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof;
@@ -305,8 +300,7 @@
| Comment => (Markup.comment, "")
| InternalValue => (Markup.empty, "")
| Error msg => (Markup.bad, msg)
- | Sync => (Markup.control, "")
- | EOF => (Markup.control, "");
+ | EOF => (Markup.empty, "");
in
@@ -339,7 +333,6 @@
| Verbatim => enclose "{*" "*}" x
| Cartouche => cartouche x
| Comment => enclose "(*" "*)" x
- | Sync => ""
| EOF => ""
| _ => x);
@@ -493,14 +486,13 @@
val scan_verb =
$$$ "*" --| Scan.ahead (~$$ "}") ||
- Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s) >> single;
+ Scan.one (fn (s, _) => s <> "*" andalso Symbol.not_eof s) >> single;
val scan_verbatim =
Scan.ahead ($$ "{" -- $$ "*") |--
!!! "unclosed verbatim text"
((Symbol_Pos.scan_pos --| $$ "{" --| $$ "*") --
- Symbol_Pos.change_prompt
- ((Scan.repeat scan_verb >> flat) -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos)));
+ ((Scan.repeat scan_verb >> flat) -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos)));
val recover_verbatim =
$$$ "{" @@@ $$$ "*" @@@ (Scan.repeat scan_verb >> flat);
@@ -550,7 +542,6 @@
scan_cartouche >> token_range Cartouche ||
scan_comment >> token_range Comment ||
scan_space >> token Space ||
- Scan.one (Symbol.is_sync o Symbol_Pos.symbol) >> (token Sync o single) ||
(Scan.max token_leq
(Scan.max token_leq
(Scan.literal lex2 >> pair Command)
@@ -570,7 +561,7 @@
recover_verbatim ||
Symbol_Pos.recover_cartouche ||
Symbol_Pos.recover_comment ||
- Scan.one (Symbol.is_regular o Symbol_Pos.symbol) >> single)
+ Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single)
>> (single o token (Error msg));
in
--- a/src/Pure/Isar/toplevel.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/Isar/toplevel.ML Fri Oct 31 23:51:54 2014 +0100
@@ -26,9 +26,6 @@
val pretty_state: state -> Pretty.T list
val print_state: state -> unit
val pretty_abstract: state -> Pretty.T
- val quiet: bool Unsynchronized.ref
- val interact: bool Unsynchronized.ref
- val timing: bool Unsynchronized.ref
val profiling: int Unsynchronized.ref
type transition
val empty: transition
@@ -213,9 +210,6 @@
(** toplevel transitions **)
-val quiet = Unsynchronized.ref false; (*Proof General legacy*)
-val interact = Unsynchronized.ref false; (*Proof General legacy*)
-val timing = Unsynchronized.ref false; (*Proof General legacy*)
val profiling = Unsynchronized.ref 0;
@@ -528,12 +522,10 @@
(fn Proof (prf, x) => Proof (f prf, x)
| _ => raise UNDEF));
-(*Proof General legacy*)
fun skip_proof f = transaction (fn _ =>
(fn Skipped_Proof (h, x) => Skipped_Proof (f h, x)
| _ => raise UNDEF));
-(*Proof General legacy*)
fun skip_proof_to_theory pred = transaction (fn _ =>
(fn Skipped_Proof (d, (gthy, _)) => if pred d then Theory (gthy, NONE) else raise UNDEF
| _ => raise UNDEF));
@@ -580,10 +572,6 @@
val (result, opt_err) =
state |> (apply_trans int trans |> ! profiling > 0 ? profile (! profiling));
- val _ =
- if int andalso not (! quiet) andalso Keyword.is_printed name
- then print_state result else ();
-
val timing_result = Timing.result timing_start;
val timing_props =
Markup.command_timing :: (Markup.nameN, name_of tr) :: Position.properties_of (pos_of tr);
@@ -627,7 +615,7 @@
if Exn.is_interrupt exn then reraise exn else raise Runtime.EXCURSION_FAIL (exn, info)
| NONE => raise Runtime.EXCURSION_FAIL (Runtime.TERMINATE, at_command tr));
-fun command tr = command_exception (! interact) tr;
+val command = command_exception false;
(* reset state *)
--- a/src/Pure/ML/ml_lex.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/ML/ml_lex.ML Fri Oct 31 23:51:54 2014 +0100
@@ -73,7 +73,7 @@
fun end_pos_of (Token ((_, pos), _)) = pos;
-(* control tokens *)
+(* stopper *)
fun mk_eof pos = Token ((pos, Position.none), (EOF, ""));
val eof = mk_eof Position.none;
@@ -236,7 +236,7 @@
Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) >> (fn ((a, b), c) => [a, b, c]);
val scan_str =
- Scan.one (fn (s, _) => Symbol.is_regular s andalso s <> "\"" andalso s <> "\\" andalso
+ Scan.one (fn (s, _) => Symbol.not_eof s andalso s <> "\"" andalso s <> "\\" andalso
(not (Symbol.is_char s) orelse Symbol.is_printable s)) >> single ||
$$$ "\\" @@@ !!! "bad escape character in string" scan_escape;
--- a/src/Pure/PIDE/command.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/PIDE/command.ML Fri Oct 31 23:51:54 2014 +0100
@@ -162,10 +162,7 @@
if is_malformed then Toplevel.malformed pos "Malformed command syntax"
else
(case Outer_Syntax.read_spans outer_syntax (resolve_files master_dir blobs span) of
- [tr] =>
- if Keyword.is_control (Toplevel.name_of tr) then
- Toplevel.malformed pos "Illegal control command"
- else Toplevel.modify_init init tr
+ [tr] => Toplevel.modify_init init tr
| [] => Toplevel.ignored (#1 (Token.range_of span))
| _ => Toplevel.malformed (#1 proper_range) "Exactly one command expected")
handle ERROR msg => Toplevel.malformed (#1 proper_range) msg
--- a/src/Pure/PIDE/markup.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/PIDE/markup.ML Fri Oct 31 23:51:54 2014 +0100
@@ -118,7 +118,6 @@
val verbatimN: string val verbatim: T
val cartoucheN: string val cartouche: T
val commentN: string val comment: T
- val controlN: string val control: T
val tokenN: string val token: bool -> Properties.T -> T
val keyword1N: string val keyword1: T
val keyword2N: string val keyword2: T
@@ -162,7 +161,6 @@
val systemN: string
val protocolN: string
val legacyN: string val legacy: T
- val promptN: string val prompt: T
val reportN: string val report: T
val no_reportN: string val no_report: T
val badN: string val bad: T
@@ -465,7 +463,6 @@
val (verbatimN, verbatim) = markup_elem "verbatim";
val (cartoucheN, cartouche) = markup_elem "cartouche";
val (commentN, comment) = markup_elem "comment";
-val (controlN, control) = markup_elem "control";
val tokenN = "token";
fun token delimited props = (tokenN, (delimitedN, print_bool delimited) :: props);
@@ -547,7 +544,6 @@
val protocolN = "protocol";
val (legacyN, legacy) = markup_elem "legacy";
-val (promptN, prompt) = markup_elem "prompt";
val (reportN, report) = markup_elem "report";
val (no_reportN, no_report) = markup_elem "no_report";
--- a/src/Pure/PIDE/markup.scala Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/PIDE/markup.scala Fri Oct 31 23:51:54 2014 +0100
@@ -264,7 +264,6 @@
val VERBATIM = "verbatim"
val CARTOUCHE = "cartouche"
val COMMENT = "comment"
- val CONTROL = "control"
/* timing */
--- a/src/Pure/PIDE/resources.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/PIDE/resources.ML Fri Oct 31 23:51:54 2014 +0100
@@ -15,7 +15,6 @@
val parse_files: string -> (theory -> Token.file list) parser
val provide: Path.T * SHA1.digest -> theory -> theory
val provide_parse_files: string -> (theory -> Token.file list * theory) parser
- val loaded_files: theory -> Path.T list
val loaded_files_current: theory -> bool
val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
val load_thy: bool -> (Toplevel.transition -> Time.time option) -> int -> Path.T ->
@@ -116,11 +115,6 @@
NONE => false
| SOME ((_, id'), _) => id = id'));
-(*Proof General legacy*)
-fun loaded_files thy =
- let val {master_dir, provided, ...} = Files.get thy
- in map (File.full_path master_dir o #1) provided end;
-
(* load theory *)
@@ -151,8 +145,6 @@
fun load_thy document last_timing update_time master_dir header text_pos text parents =
let
- val time = ! Toplevel.timing;
-
val {name = (name, _), ...} = header;
val _ = Thy_Header.define_keywords header;
@@ -166,10 +158,9 @@
|> Present.begin_theory update_time
(fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
- val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
val (results, thy) =
- cond_timeit time "" (fn () => excursion master_dir last_timing init elements);
- val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
+ cond_timeit true ("theory " ^ quote name)
+ (fn () => excursion master_dir last_timing init elements);
fun present () =
let
--- a/src/Pure/PIDE/xml.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/PIDE/xml.ML Fri Oct 31 23:51:54 2014 +0100
@@ -192,8 +192,8 @@
val blanks = Scan.many Symbol.is_blank;
val special = $$ "&" ^^ (parse_name >> implode) ^^ $$ ";" >> decode;
-val regular = Scan.one Symbol.is_regular;
-fun regular_except x = Scan.one (fn c => Symbol.is_regular c andalso c <> x);
+val regular = Scan.one Symbol.not_eof;
+fun regular_except x = Scan.one (fn c => Symbol.not_eof c andalso c <> x);
val parse_chars = Scan.repeat1 (special || regular_except "<") >> implode;
--- a/src/Pure/Proof/extraction.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/Proof/extraction.ML Fri Oct 31 23:51:54 2014 +0100
@@ -121,7 +121,7 @@
fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs));
fun corr_name s vs = extr_name s vs ^ "_correctness";
-fun msg d s = Output.urgent_message (Pretty.spaces d ^ s);
+fun msg d s = writeln (Pretty.spaces d ^ s);
fun vars_of t = map Var (rev (Term.add_vars t []));
fun frees_of t = map Free (rev (Term.add_frees t []));
--- a/src/Pure/Pure.thy Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/Pure.thy Fri Oct 31 23:51:54 2014 +0100
@@ -79,30 +79,23 @@
and "also" "moreover" :: prf_decl % "proof"
and "finally" "ultimately" :: prf_chain % "proof"
and "back" :: prf_script % "proof"
- and "Isabelle.command" :: control
and "help" "print_commands" "print_options" "print_context"
"print_theory" "print_syntax" "print_abbrevs" "print_defn_rules"
"print_theorems" "print_locales" "print_classes" "print_locale"
"print_interps" "print_dependencies" "print_attributes"
"print_simpset" "print_rules" "print_trans_rules" "print_methods"
"print_antiquotations" "print_ML_antiquotations" "thy_deps"
- "locale_deps" "class_deps" "thm_deps" "print_binds" "print_term_bindings"
+ "locale_deps" "class_deps" "thm_deps" "print_term_bindings"
"print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf"
"prop" "term" "typ" "print_codesetup" "unused_thms" :: diag
- and "use_thy" "remove_thy" "kill_thy" :: control
- and "display_drafts" "print_state" "pr" :: diag
- and "pretty_setmargin" "disable_pr" "enable_pr" "commit" "quit" "exit" :: control
+ and "display_drafts" "print_state" :: diag
and "welcome" :: diag
- and "init_toplevel" "linear_undo" "undo" "undos_proof" "cannot_undo" "kill" :: control
and "end" :: thy_end % "theory"
and "realizers" :: thy_decl == ""
and "realizability" :: thy_decl == ""
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 +110,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 Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/ROOT Fri Oct 31 23:51:54 2014 +0100
@@ -196,7 +196,6 @@
"System/invoke_scala.ML"
"System/isabelle_process.ML"
"System/isabelle_system.ML"
- "System/isar.ML"
"System/message_channel.ML"
"System/options.ML"
"System/system_channel.ML"
@@ -211,7 +210,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 Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/ROOT.ML Fri Oct 31 23:51:54 2014 +0100
@@ -327,14 +327,12 @@
use "System/isabelle_process.ML";
use "System/invoke_scala.ML";
use "PIDE/protocol.ML";
-use "System/isar.ML";
(* miscellaneous tools and packages for Pure Isabelle *)
use "Tools/build.ML";
use "Tools/named_thms.ML";
-use "Tools/proof_general.ML";
structure Output: OUTPUT = Output; (*seal system channels!*)
--- a/src/Pure/Syntax/lexicon.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/Syntax/lexicon.ML Fri Oct 31 23:51:54 2014 +0100
@@ -230,7 +230,7 @@
val scan_chr =
$$ "\\" |-- $$$ "'" ||
Scan.one
- ((fn s => s <> "\\" andalso s <> "'" andalso Symbol.is_regular s) o
+ ((fn s => s <> "\\" andalso s <> "'" andalso Symbol.not_eof s) o
Symbol_Pos.symbol) >> single ||
$$$ "'" --| Scan.ahead (~$$ "'");
@@ -339,7 +339,7 @@
val scan =
$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof)
>> Syntax.var ||
- Scan.many (Symbol.is_regular o Symbol_Pos.symbol)
+ Scan.many (Symbol.not_eof o Symbol_Pos.symbol)
>> (Syntax.free o implode o map Symbol_Pos.symbol);
in the (Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none))) end;
--- a/src/Pure/Syntax/syntax_ext.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/Syntax/syntax_ext.ML Fri Oct 31 23:51:54 2014 +0100
@@ -143,8 +143,8 @@
val is_meta = member (op =) ["(", ")", "/", "_", "\\<index>"];
val scan_delim_char =
- $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.is_regular) ||
- Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.is_regular);
+ $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.not_eof) ||
+ Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof);
fun read_int ["0", "0"] = ~1
| read_int cs = #1 (Library.read_int cs);
--- a/src/Pure/System/isabelle_process.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/System/isabelle_process.ML Fri Oct 31 23:51:54 2014 +0100
@@ -126,8 +126,6 @@
(fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
Output.system_message_fn := message Markup.systemN [];
Output.protocol_message_fn := message Markup.protocolN;
- Output.urgent_message_fn := ! Output.writeln_fn;
- Output.prompt_fn := ignore;
message Markup.initN [] [Session.welcome ()];
msg_channel
end;
@@ -205,7 +203,7 @@
val channel = rendezvous ();
val msg_channel = init_channels channel;
val _ = Session.init_protocol_handlers ();
- val _ = (loop |> Unsynchronized.setmp Toplevel.quiet true) channel;
+ val _ = loop channel;
in Message_Channel.shutdown msg_channel end);
fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);
--- a/src/Pure/System/isar.ML Fri Oct 31 17:01:54 2014 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,174 +0,0 @@
-(* Title: Pure/System/isar.ML
- Author: Makarius
-
-Global state of the raw Isar read-eval-print loop.
-*)
-
-signature ISAR =
-sig
- val init: unit -> unit
- val exn: unit -> (exn * string) option
- val state: unit -> Toplevel.state
- val goal: unit -> {context: Proof.context, facts: thm list, goal: thm}
- val print: unit -> unit
- val >> : Toplevel.transition -> bool
- val >>> : Toplevel.transition list -> unit
- val linear_undo: int -> unit
- val undo: int -> unit
- val kill: unit -> unit
- val kill_proof: unit -> unit
- val crashes: exn list Synchronized.var
- val toplevel_loop: TextIO.instream ->
- {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
- val loop: unit -> unit
- val main: unit -> unit
-end;
-
-structure Isar: ISAR =
-struct
-
-
-(** TTY model -- SINGLE-THREADED! **)
-
-(* the global state *)
-
-type history = (Toplevel.state * Toplevel.transition) list;
- (*previous state, state transition -- regular commands only*)
-
-local
- val global_history = Unsynchronized.ref ([]: history);
- val global_state = Unsynchronized.ref Toplevel.toplevel;
- val global_exn = Unsynchronized.ref (NONE: (exn * string) option);
-in
-
-fun edit_history count f = NAMED_CRITICAL "Isar" (fn () =>
- let
- fun edit 0 (st, hist) = (global_history := hist; global_state := st; global_exn := NONE)
- | edit n (st, hist) = edit (n - 1) (f st hist);
- in edit count (! global_state, ! global_history) end);
-
-fun state () = ! global_state;
-
-fun exn () = ! global_exn;
-fun set_exn exn = global_exn := exn;
-
-end;
-
-
-fun init () = edit_history 1 (K (K (Toplevel.toplevel, [])));
-
-fun goal () = Proof.goal (Toplevel.proof_of (state ()))
- handle Toplevel.UNDEF => error "No goal present";
-
-fun print () = Toplevel.print_state (state ());
-
-
-(* history navigation *)
-
-local
-
-fun find_and_undo _ [] = error "Undo history exhausted"
- | find_and_undo which ((prev, tr) :: hist) =
- if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist;
-
-in
-
-fun linear_undo n = edit_history n (K (find_and_undo (K true)));
-
-fun undo n = edit_history n (fn st => fn hist =>
- find_and_undo (if Toplevel.is_proof st then K true else Keyword.is_theory) hist);
-
-fun kill () = edit_history 1 (fn st => fn hist =>
- find_and_undo
- (if Toplevel.is_proof st then Keyword.is_theory else Keyword.is_theory_begin) hist);
-
-fun kill_proof () = edit_history 1 (fn st => fn hist =>
- if Toplevel.is_proof st then find_and_undo Keyword.is_theory hist
- else raise Toplevel.UNDEF);
-
-end;
-
-
-(* interactive state transformations *)
-
-fun op >> tr =
- (case Toplevel.transition true tr (state ()) of
- NONE => false
- | SOME (_, SOME exn_info) =>
- (set_exn (SOME exn_info);
- Toplevel.setmp_thread_position tr
- Runtime.exn_error_message (Runtime.EXCURSION_FAIL exn_info);
- true)
- | SOME (st', NONE) =>
- let
- val name = Toplevel.name_of tr;
- val _ = if Keyword.is_theory_begin name then init () else ();
- val _ =
- if Keyword.is_regular name
- then edit_history 1 (fn st => fn hist => (st', (st, tr) :: hist)) else ();
- in true end);
-
-fun op >>> [] = ()
- | op >>> (tr :: trs) = if op >> tr then op >>> trs else ();
-
-
-(* toplevel loop -- uninterruptible *)
-
-val crashes = Synchronized.var "Isar.crashes" ([]: exn list);
-
-local
-
-fun protocol_message props output =
- (case props of
- function :: args =>
- if function = Markup.command_timing then
- let
- val name = the_default "" (Properties.get args Markup.nameN);
- val pos = Position.of_properties args;
- val timing = Markup.parse_timing_properties args;
- in
- if Timing.is_relevant timing andalso (! Toplevel.profiling > 0 orelse ! Toplevel.timing)
- andalso name <> "" andalso not (Keyword.is_control name)
- then tracing ("command " ^ quote name ^ Position.here pos ^ ": " ^ Timing.message timing)
- else ()
- end
- else raise Output.Protocol_Message props
- | [] => raise Output.Protocol_Message props);
-
-fun raw_loop secure src =
- let
- fun check_secure () =
- (if secure then warning "Secure loop -- cannot exit to ML" else (); secure);
- in
- (case Source.get_single (Source.set_prompt Source.default_prompt src) of
- NONE => if secure then quit () else ()
- | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
- handle exn =>
- (Runtime.exn_error_message exn
- handle crash =>
- (Synchronized.change crashes (cons crash);
- warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
- raw_loop secure src)
- end;
-
-in
-
-fun toplevel_loop in_stream {init = do_init, welcome, sync, secure} =
- (Context.set_thread_data NONE;
- Multithreading.max_threads_update (Options.default_int "threads");
- if do_init then init () else ();
- Output.protocol_message_fn := protocol_message;
- if welcome then writeln (Session.welcome ()) else ();
- uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ());
-
-end;
-
-fun loop () =
- toplevel_loop TextIO.stdIn
- {init = false, welcome = false, sync = false, secure = Secure.is_secure ()};
-
-fun main () =
- toplevel_loop TextIO.stdIn
- {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};
-
-end;
--- a/src/Pure/System/message_channel.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/System/message_channel.ML Fri Oct 31 23:51:54 2014 +0100
@@ -51,8 +51,7 @@
[] => (flush channel; continue NONE)
| msgs => received timeout msgs)
and received _ (NONE :: _) = flush channel
- | received timeout (SOME msg :: rest) =
- (output_message channel msg; received flush_timeout rest)
+ | received _ (SOME msg :: rest) = (output_message channel msg; received flush_timeout rest)
| received timeout [] = continue timeout;
in fn () => continue NONE end;
--- a/src/Pure/Thy/thy_info.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/Thy/thy_info.ML Fri Oct 31 23:51:54 2014 +0100
@@ -14,7 +14,6 @@
val get_theory: string -> theory
val is_finished: string -> bool
val master_directory: string -> Path.T
- val loaded_files: string -> Path.T list
val remove_thy: string -> unit
val kill_thy: string -> unit
val use_theories:
@@ -22,8 +21,7 @@
(string * Position.T) list -> unit
val use_thys: (string * Position.T) list -> unit
val use_thy: string * Position.T -> unit
- val script_thy: Position.T -> string -> theory
- val toplevel_begin_theory: Path.T -> Thy_Header.header -> theory
+ val script_thy: Position.T -> string -> theory -> theory
val register_thy: theory -> unit
val finish: unit -> unit
end;
@@ -126,12 +124,6 @@
val get_imports = Resources.imports_of o get_theory;
-(*Proof General legacy*)
-fun loaded_files name = NAMED_CRITICAL "Thy_Info" (fn () =>
- (case get_deps name of
- NONE => []
- | SOME {master = (thy_path, _), ...} => thy_path :: Resources.loaded_files (get_theory name)));
-
(** thy operations **)
@@ -143,7 +135,7 @@
else
let
val succs = thy_graph String_Graph.all_succs [name];
- val _ = Output.urgent_message ("Theory loader: removing " ^ commas_quote succs);
+ val _ = writeln ("Theory loader: removing " ^ commas_quote succs);
val _ = List.app (perform Remove) succs;
val _ = change_thys (fold String_Graph.del_node succs);
in () end);
@@ -269,7 +261,7 @@
fun load_thy document last_timing initiators update_time deps text (name, pos) keywords parents =
let
val _ = kill_thy name;
- val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
+ val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators);
val _ = Output.try_protocol_message (Markup.loading_theory name) [];
val {master = (thy_path, _), imports} = deps;
@@ -378,22 +370,15 @@
(* toplevel scripting -- without maintaining database *)
-fun script_thy pos txt =
+fun script_thy pos txt thy =
let
- val trs = Outer_Syntax.parse (Outer_Syntax.get_syntax ()) pos txt;
+ val trs =
+ Outer_Syntax.parse (Outer_Syntax.get_syntax ()) pos txt
+ |> map (Toplevel.modify_init (K thy));
val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs);
val end_state = fold (Toplevel.command_exception true) trs Toplevel.toplevel;
in Toplevel.end_theory end_pos end_state end;
-fun toplevel_begin_theory master_dir (header: Thy_Header.header) =
- let
- val {name = (name, _), imports, ...} = header;
- val _ = kill_thy name;
- val _ = use_theories {document = false, last_timing = K NONE, master_dir = master_dir} imports;
- val _ = Thy_Header.define_keywords header;
- val parents = map (get_theory o base_name o fst) imports;
- in Resources.begin_theory master_dir header parents end;
-
(* register theory *)
@@ -405,7 +390,7 @@
in
NAMED_CRITICAL "Thy_Info" (fn () =>
(kill_thy name;
- Output.urgent_message ("Registering theory " ^ quote name);
+ writeln ("Registering theory " ^ quote name);
update_thy (make_deps master imports) theory))
end;
--- a/src/Pure/Tools/build.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/Tools/build.ML Fri Oct 31 23:51:54 2014 +0100
@@ -108,8 +108,7 @@
|> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
|> Multithreading.max_threads_setmp (Options.int options "threads")
|> Unsynchronized.setmp Future.ML_statistics true
- |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
- |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
+ |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin");
fun use_theories_condition last_timing (options, thys) =
let val condition = space_explode "," (Options.string options "condition") in
--- a/src/Pure/Tools/keywords.scala Fri Oct 31 17:01:54 2014 +0000
+++ /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 Fri Oct 31 17:01:54 2014 +0000
+++ /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/Tools/proof_general_pure.ML Fri Oct 31 17:01:54 2014 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,227 +0,0 @@
-(* Title: Pure/Tools/proof_general_pure.ML
- Author: David Aspinall
- Author: Makarius
-
-Proof General setup within theory Pure.
-*)
-
-(*Proof General legacy*)
-
-structure ProofGeneral_Pure: sig end =
-struct
-
-(** preferences **)
-
-(* display *)
-
-val _ =
- ProofGeneral.preference_option ProofGeneral.category_display
- NONE
- @{system_option show_types}
- "show-types"
- "Include types in display of Isabelle terms";
-
-val _ =
- ProofGeneral.preference_option ProofGeneral.category_display
- NONE
- @{system_option show_sorts}
- "show-sorts"
- "Include sorts in display of Isabelle types";
-
-val _ =
- ProofGeneral.preference_option ProofGeneral.category_display
- NONE
- @{system_option show_consts}
- "show-consts"
- "Show types of consts in Isabelle goal display";
-
-val _ =
- ProofGeneral.preference_option ProofGeneral.category_display
- NONE
- @{system_option names_long}
- "long-names"
- "Show fully qualified names in Isabelle terms";
-
-val _ =
- ProofGeneral.preference_option ProofGeneral.category_display
- NONE
- @{system_option show_brackets}
- "show-brackets"
- "Show full bracketing in Isabelle terms";
-
-val _ =
- ProofGeneral.preference_option ProofGeneral.category_display
- NONE
- @{system_option show_main_goal}
- "show-main-goal"
- "Show main goal in proof state display";
-
-val _ =
- ProofGeneral.preference_option ProofGeneral.category_display
- NONE
- @{system_option eta_contract}
- "eta-contract"
- "Print terms eta-contracted";
-
-
-(* advanced display *)
-
-val _ =
- ProofGeneral.preference_option ProofGeneral.category_advanced_display
- NONE
- @{system_option goals_limit}
- "goals-limit"
- "Setting for maximum number of subgoals to be printed";
-
-val _ =
- ProofGeneral.preference ProofGeneral.category_advanced_display
- NONE
- (Markup.print_int o get_default_print_depth)
- (default_print_depth o Markup.parse_int)
- ProofGeneral.pgipint
- "print-depth"
- "Setting for the ML print depth";
-
-val _ =
- ProofGeneral.preference_option ProofGeneral.category_advanced_display
- NONE
- @{system_option show_question_marks}
- "show-question-marks"
- "Show leading question mark of variable name";
-
-
-(* tracing *)
-
-val _ =
- ProofGeneral.preference_bool ProofGeneral.category_tracing
- NONE
- Raw_Simplifier.simp_trace_default
- "trace-simplifier"
- "Trace simplification rules";
-
-val _ =
- ProofGeneral.preference_int ProofGeneral.category_tracing
- NONE
- Raw_Simplifier.simp_trace_depth_limit_default
- "trace-simplifier-depth"
- "Trace simplifier depth limit";
-
-val _ =
- ProofGeneral.preference_bool ProofGeneral.category_tracing
- NONE
- Pattern.unify_trace_failure_default
- "trace-unification"
- "Output error diagnostics during unification";
-
-val _ =
- ProofGeneral.preference_bool ProofGeneral.category_tracing
- NONE
- Toplevel.timing
- "global-timing"
- "Whether to enable timing in Isabelle";
-
-val _ =
- ProofGeneral.preference_option ProofGeneral.category_tracing
- NONE
- @{system_option ML_exception_trace}
- "debugging"
- "Whether to enable exception trace for toplevel command execution";
-
-val _ =
- ProofGeneral.preference_bool ProofGeneral.category_tracing
- NONE
- ProofGeneral.thm_deps
- "theorem-dependencies"
- "Track theorem dependencies within Proof General";
-
-
-(* proof *)
-
-val _ =
- ProofGeneral.preference_option ProofGeneral.category_proof
- (SOME "true")
- @{system_option quick_and_dirty}
- "quick-and-dirty"
- "Take a few short cuts";
-
-val _ =
- ProofGeneral.preference_option ProofGeneral.category_proof
- NONE
- @{system_option skip_proofs}
- "skip-proofs"
- "Skip over proofs";
-
-val _ =
- ProofGeneral.preference ProofGeneral.category_proof
- NONE
- (Markup.print_bool o Proofterm.proofs_enabled)
- (fn s => Proofterm.proofs := (if Markup.parse_bool s then 2 else 0))
- ProofGeneral.pgipbool
- "full-proofs"
- "Record full proof objects internally";
-
-val _ =
- ProofGeneral.preference ProofGeneral.category_proof
- NONE
- (Markup.print_int o Multithreading.max_threads_value)
- (Multithreading.max_threads_update o Markup.parse_int)
- ProofGeneral.pgipint
- "max-threads"
- "Maximum number of threads";
-
-val _ =
- ProofGeneral.preference ProofGeneral.category_proof
- NONE
- (fn () => Markup.print_bool (! Goal.parallel_proofs >= 1))
- (fn s => Goal.parallel_proofs := (if Markup.parse_bool s then 1 else 0))
- ProofGeneral.pgipint
- "parallel-proofs"
- "Check proofs in parallel";
-
-
-
-(** command syntax **)
-
-val _ =
- Outer_Syntax.improper_command
- @{command_spec "ProofGeneral.process_pgip"} "(internal)"
- (Parse.text >> (fn str => Toplevel.imperative (fn () => ProofGeneral.process_pgip str)));
-
-val _ =
- Outer_Syntax.improper_command
- @{command_spec "ProofGeneral.pr"} "(internal)"
- (Scan.succeed (Toplevel.keep (fn state =>
- if Toplevel.is_toplevel state orelse Toplevel.is_theory state
- then ProofGeneral.tell_clear_goals ()
- else (Toplevel.quiet := false; Toplevel.print_state state))));
-
-val _ = (*undo without output -- historical*)
- Outer_Syntax.improper_command
- @{command_spec "ProofGeneral.undo"} "(internal)"
- (Scan.succeed (Toplevel.imperative (fn () => Isar.undo 1)));
-
-val _ =
- Outer_Syntax.improper_command
- @{command_spec "ProofGeneral.restart"} "(internal)"
- (Parse.opt_unit >> (K (Toplevel.imperative ProofGeneral.restart)));
-
-val _ =
- Outer_Syntax.improper_command
- @{command_spec "ProofGeneral.kill_proof"} "(internal)"
- (Scan.succeed (Toplevel.imperative (fn () =>
- (Isar.kill_proof (); ProofGeneral.tell_clear_goals ()))));
-
-val _ =
- Outer_Syntax.improper_command
- @{command_spec "ProofGeneral.inform_file_processed"} "(internal)"
- (Parse.name >> (fn file => Toplevel.imperative (fn () =>
- ProofGeneral.inform_file_processed file)));
-
-val _ =
- Outer_Syntax.improper_command
- @{command_spec "ProofGeneral.inform_file_retracted"} "(internal)"
- (Parse.name >> (fn file => Toplevel.imperative (fn () =>
- ProofGeneral.inform_file_retracted file)));
-
-end;
-
--- a/src/Pure/build-jars Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/build-jars Fri Oct 31 23:51:54 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 Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Pure/pure_syn.ML Fri Oct 31 23:51:54 2014 +0100
@@ -10,9 +10,8 @@
val _ =
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)));
+ (Thy_Header.args >>
+ (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization")));
val _ =
Outer_Syntax.command
--- a/src/Tools/Code/code_printer.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Tools/Code/code_printer.ML Fri Oct 31 23:51:54 2014 +0100
@@ -373,7 +373,7 @@
fun read_mixfix s =
let
- val sym_any = Scan.one Symbol.is_regular;
+ val sym_any = Scan.one Symbol.not_eof;
val parse = Scan.optional ($$ "!" >> K NOBR) BR -- Scan.repeat (
($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))
|| ($$ "_" >> K (Arg BR))
--- a/src/Tools/quickcheck.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Tools/quickcheck.ML Fri Oct 31 23:51:54 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
@@ -304,11 +294,11 @@
if is_interactive then exc () else raise TimeLimit.TimeOut
else f ();
-fun message ctxt s = if Config.get ctxt quiet then () else Output.urgent_message s;
+fun message ctxt s = if Config.get ctxt quiet then () else writeln s;
fun verbose_message ctxt s =
if not (Config.get ctxt quiet) andalso Config.get ctxt verbose
- then Output.urgent_message s else ();
+ then writeln s else ();
fun test_terms ctxt (limit_time, is_interactive) insts goals =
(case active_testers ctxt of
@@ -527,7 +517,7 @@
gen_quickcheck args i (Toplevel.proof_of state)
|> apfst (Option.map (the o get_first response_of))
|> (fn (r, state) =>
- Output.urgent_message (Pretty.string_of
+ writeln (Pretty.string_of
(pretty_counterex (Proof.context_of state) false r)));
val parse_arg =
@@ -573,7 +563,7 @@
|> (if auto then
Proof.goal_message (K (Pretty.mark Markup.information msg))
else
- tap (fn _ => Output.urgent_message (Pretty.string_of msg))))
+ tap (fn _ => writeln (Pretty.string_of msg))))
else
(noneN, state)
end)
--- a/src/Tools/solve_direct.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Tools/solve_direct.ML Fri Oct 31 23:51:54 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 *)
@@ -90,13 +83,13 @@
Pretty.markup Markup.information (message results))
else
tap (fn _ =>
- Output.urgent_message (Pretty.string_of (Pretty.chunks (message results))))))
+ writeln (Pretty.string_of (Pretty.chunks (message results))))))
| SOME NONE =>
- (if mode = Normal then Output.urgent_message "No proof found."
+ (if mode = Normal then writeln "No proof found."
else ();
(noneN, state))
| NONE =>
- (if mode = Normal then Output.urgent_message "An error occurred."
+ (if mode = Normal then writeln "An error occurred."
else ();
(unknownN, state)))
end
--- a/src/Tools/try.ML Fri Oct 31 17:01:54 2014 +0000
+++ b/src/Tools/try.ML Fri Oct 31 23:51:54 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 _ [] = ["??"]
@@ -70,19 +60,19 @@
fun try_tools state =
if subgoal_count state = 0 then
- (Output.urgent_message "No subgoal!"; NONE)
+ (writeln "No subgoal!"; NONE)
else
get_tools (Proof.theory_of state)
|> tap (fn tools =>
"Trying " ^ space_implode " "
(serial_commas "and" (map (quote o fst) tools)) ^ "..."
- |> Output.urgent_message)
+ |> writeln)
|> Par_List.get_some
(fn (name, (_, _, tool)) =>
case try (tool false) state of
SOME (true, (outcome_code, _)) => SOME (name, outcome_code)
| _ => NONE)
- |> tap (fn NONE => Output.urgent_message "Tried in vain." | _ => ())
+ |> tap (fn NONE => writeln "Tried in vain." | _ => ())
val _ =
Outer_Syntax.improper_command @{command_spec "try"}
@@ -101,17 +91,6 @@
| _ => NONE)
|> the_default state
-val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
- let
- val auto_time_limit = Options.default_real @{system_option auto_time_limit}
- in
- if interact andalso not (!Toplevel.quiet) andalso auto_time_limit > 0.0 then
- TimeLimit.timeLimit (seconds auto_time_limit) auto_try state
- handle TimeLimit.TimeOut => state
- else
- state
- end))
-
(* asynchronous print function (PIDE) *)