--- a/NEWS Sun Apr 06 17:18:57 2014 +0200
+++ b/NEWS Sun Apr 06 17:19:08 2014 +0200
@@ -662,6 +662,13 @@
repeated invocation in PIDE front-end: re-use single file
$ISABELLE_HOME_USER/tmp/drafts.pdf and corresponding views.
+* The raw Isabelle process executable has been renamed from
+"isabelle-process" to "isabelle_process", which conforms to common
+shell naming conventions, and allows to define a shell function within
+the Isabelle environment to avoid dynamic path lookup. Rare
+incompatibility for old tools that do not use the $ISABELLE_PROCESS
+settings variable yet.
+
New in Isabelle2013-2 (December 2013)
--- a/bin/isabelle-process Sun Apr 06 17:18:57 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,249 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# Isabelle process startup script.
-
-if [ -L "$0" ]; then
- TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
- exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
-fi
-
-
-## settings
-
-PRG="$(basename "$0")"
-
-ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
-source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
-
-
-## diagnostics
-
-function usage()
-{
- echo
- echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
- echo
- echo " Options are:"
- echo " -I startup Isar interaction mode"
- 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"
- echo " -e MLTEXT pass MLTEXT to the ML session"
- echo " -m MODE add print mode for output"
- echo " -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)"
- echo " -q non-interactive session"
- echo " -r open heap file read-only"
- echo " -w reset write permissions on OUTPUT"
- echo
- echo " INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps."
- echo " These are either names to be searched in the Isabelle path, or"
- echo " actual file names (containing at least one /)."
- echo " If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-## process command line
-
-# options
-
-ISAR=""
-PROOFGENERAL=""
-SECURE=""
-WRAPPER_SOCKET=""
-WRAPPER_FIFOS=""
-MLTEXT=""
-MODES=""
-declare -a SYSTEM_OPTIONS=()
-TERMINATE=""
-READONLY=""
-NOWRITE=""
-
-while getopts "IPST:W:e:m:o:qrw" OPT
-do
- case "$OPT" in
- I)
- ISAR=true
- ;;
- P)
- PROOFGENERAL=true
- ;;
- S)
- SECURE=true
- ;;
- T)
- WRAPPER_SOCKET="$OPTARG"
- ;;
- W)
- WRAPPER_FIFOS="$OPTARG"
- ;;
- e)
- MLTEXT="$MLTEXT $OPTARG"
- ;;
- m)
- if [ -z "$MODES" ]; then
- MODES="\"$OPTARG\""
- else
- MODES="\"$OPTARG\", $MODES"
- fi
- ;;
- o)
- SYSTEM_OPTIONS["${#SYSTEM_OPTIONS[@]}"]="$OPTARG"
- ;;
- q)
- TERMINATE=true
- ;;
- r)
- READONLY=true
- ;;
- w)
- NOWRITE=true
- ;;
- \?)
- usage
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-INPUT=""
-OUTPUT=""
-
-if [ "$#" -ge 1 ]; then
- INPUT="$1"
- shift
-fi
-
-if [ "$#" -ge 1 ]; then
- OUTPUT="$1"
- shift
-fi
-
-[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
-
-
-## check ML system
-
-[ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
-
-
-## input heap file
-
-[ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"
-
-case "$INPUT" in
- RAW_ML_SYSTEM)
- INFILE=""
- ;;
- */*)
- INFILE="$INPUT"
- [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
- ;;
- *)
- INFILE=""
- ISA_PATH=""
-
- splitarray ":" "$ISABELLE_PATH"; PATHS=("${SPLITARRAY[@]}")
- for DIR in "${PATHS[@]}"
- do
- DIR="$DIR/$ML_IDENTIFIER"
- ISA_PATH="$ISA_PATH $DIR\n"
- [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
- done
-
- if [ -z "$INFILE" ]; then
- echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
- echo -ne "$ISA_PATH" >&2
- exit 2
- fi
- ;;
-esac
-
-
-## output heap file
-
-case "$OUTPUT" in
- "")
- if [ -z "$READONLY" -a -w "$INFILE" ]; then
- perl -e "exit (((stat('$INFILE'))[2] & 0222) != 0 ? 0 : 1);" && OUTFILE="$INFILE"
- fi
- ;;
- */*)
- OUTFILE="$OUTPUT"
- ;;
- *)
- mkdir -p "$ISABELLE_OUTPUT"
- OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
- ;;
-esac
-
-
-## prepare tmp directory
-
-[ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
-ISABELLE_PID="$$"
-ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID"
-mkdir -p "$ISABELLE_TMP"
-
-
-## run it!
-
-ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
-
-[ -n "$MODES" ] && MLTEXT="Unsynchronized.change print_mode (append [$MODES]); $MLTEXT"
-
-[ -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
- splitarray ":" "$WRAPPER_FIFOS"; FIFOS=("${SPLITARRAY[@]}")
- [ "${#FIFOS[@]}" -eq 2 ] || fail "Expected IN:OUT fifo specification"
- [ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}"
- [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}"
- MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
-else
- ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options"
- "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" -- "${SYSTEM_OPTIONS[@]}" || \
- fail "Failed to retrieve Isabelle system options"
- if [ "$INPUT" != RAW_ML_SYSTEM -a "$INPUT" != RAW ]; then
- MLTEXT="Options.load_default () handle _ => exit 2; $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"
-else
- $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
-fi
-RC="$?"
-
-[ -n "$ISABELLE_PROCESS_OPTIONS" ] && rm -f "$ISABELLE_PROCESS_OPTIONS"
-rmdir "$ISABELLE_TMP"
-
-exit "$RC"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/bin/isabelle_process Sun Apr 06 17:19:08 2014 +0200
@@ -0,0 +1,249 @@
+#!/usr/bin/env bash
+#
+# Author: Markus Wenzel, TU Muenchen
+#
+# Isabelle process startup script.
+
+if [ -L "$0" ]; then
+ TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
+ exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
+fi
+
+
+## settings
+
+PRG="$(basename "$0")"
+
+ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
+source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
+
+
+## diagnostics
+
+function usage()
+{
+ echo
+ echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
+ echo
+ echo " Options are:"
+ echo " -I startup Isar interaction mode"
+ 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"
+ echo " -e MLTEXT pass MLTEXT to the ML session"
+ echo " -m MODE add print mode for output"
+ echo " -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)"
+ echo " -q non-interactive session"
+ echo " -r open heap file read-only"
+ echo " -w reset write permissions on OUTPUT"
+ echo
+ echo " INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps."
+ echo " These are either names to be searched in the Isabelle path, or"
+ echo " actual file names (containing at least one /)."
+ echo " If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system."
+ echo
+ exit 1
+}
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+
+## process command line
+
+# options
+
+ISAR=""
+PROOFGENERAL=""
+SECURE=""
+WRAPPER_SOCKET=""
+WRAPPER_FIFOS=""
+MLTEXT=""
+MODES=""
+declare -a SYSTEM_OPTIONS=()
+TERMINATE=""
+READONLY=""
+NOWRITE=""
+
+while getopts "IPST:W:e:m:o:qrw" OPT
+do
+ case "$OPT" in
+ I)
+ ISAR=true
+ ;;
+ P)
+ PROOFGENERAL=true
+ ;;
+ S)
+ SECURE=true
+ ;;
+ T)
+ WRAPPER_SOCKET="$OPTARG"
+ ;;
+ W)
+ WRAPPER_FIFOS="$OPTARG"
+ ;;
+ e)
+ MLTEXT="$MLTEXT $OPTARG"
+ ;;
+ m)
+ if [ -z "$MODES" ]; then
+ MODES="\"$OPTARG\""
+ else
+ MODES="\"$OPTARG\", $MODES"
+ fi
+ ;;
+ o)
+ SYSTEM_OPTIONS["${#SYSTEM_OPTIONS[@]}"]="$OPTARG"
+ ;;
+ q)
+ TERMINATE=true
+ ;;
+ r)
+ READONLY=true
+ ;;
+ w)
+ NOWRITE=true
+ ;;
+ \?)
+ usage
+ ;;
+ esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+INPUT=""
+OUTPUT=""
+
+if [ "$#" -ge 1 ]; then
+ INPUT="$1"
+ shift
+fi
+
+if [ "$#" -ge 1 ]; then
+ OUTPUT="$1"
+ shift
+fi
+
+[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
+
+
+## check ML system
+
+[ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle."
+
+
+## input heap file
+
+[ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC"
+
+case "$INPUT" in
+ RAW_ML_SYSTEM)
+ INFILE=""
+ ;;
+ */*)
+ INFILE="$INPUT"
+ [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
+ ;;
+ *)
+ INFILE=""
+ ISA_PATH=""
+
+ splitarray ":" "$ISABELLE_PATH"; PATHS=("${SPLITARRAY[@]}")
+ for DIR in "${PATHS[@]}"
+ do
+ DIR="$DIR/$ML_IDENTIFIER"
+ ISA_PATH="$ISA_PATH $DIR\n"
+ [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
+ done
+
+ if [ -z "$INFILE" ]; then
+ echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
+ echo -ne "$ISA_PATH" >&2
+ exit 2
+ fi
+ ;;
+esac
+
+
+## output heap file
+
+case "$OUTPUT" in
+ "")
+ if [ -z "$READONLY" -a -w "$INFILE" ]; then
+ perl -e "exit (((stat('$INFILE'))[2] & 0222) != 0 ? 0 : 1);" && OUTFILE="$INFILE"
+ fi
+ ;;
+ */*)
+ OUTFILE="$OUTPUT"
+ ;;
+ *)
+ mkdir -p "$ISABELLE_OUTPUT"
+ OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
+ ;;
+esac
+
+
+## prepare tmp directory
+
+[ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
+ISABELLE_PID="$$"
+ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID"
+mkdir -p "$ISABELLE_TMP"
+
+
+## run it!
+
+ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
+
+[ -n "$MODES" ] && MLTEXT="Unsynchronized.change print_mode (append [$MODES]); $MLTEXT"
+
+[ -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
+ splitarray ":" "$WRAPPER_FIFOS"; FIFOS=("${SPLITARRAY[@]}")
+ [ "${#FIFOS[@]}" -eq 2 ] || fail "Expected IN:OUT fifo specification"
+ [ -p "${FIFOS[0]}" ] || fail "Bad input fifo: ${FIFOS[0]}"
+ [ -p "${FIFOS[1]}" ] || fail "Bad output fifo: ${FIFOS[1]}"
+ MLTEXT="$MLTEXT; Isabelle_Process.init_fifos \"${FIFOS[0]}\" \"${FIFOS[1]}\";"
+else
+ ISABELLE_PROCESS_OPTIONS="$ISABELLE_TMP/options"
+ "$ISABELLE_TOOL" options -x "$ISABELLE_PROCESS_OPTIONS" -- "${SYSTEM_OPTIONS[@]}" || \
+ fail "Failed to retrieve Isabelle system options"
+ if [ "$INPUT" != RAW_ML_SYSTEM -a "$INPUT" != RAW ]; then
+ MLTEXT="Options.load_default () handle _ => exit 2; $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"
+else
+ $NICE "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
+fi
+RC="$?"
+
+[ -n "$ISABELLE_PROCESS_OPTIONS" ] && rm -f "$ISABELLE_PROCESS_OPTIONS"
+rmdir "$ISABELLE_TMP"
+
+exit "$RC"
--- a/lib/Tools/install Sun Apr 06 17:18:57 2014 +0200
+++ b/lib/Tools/install Sun Apr 06 17:19:08 2014 +0200
@@ -63,7 +63,7 @@
mkdir -p "$BINDIR" || fail "Bad directory: \"$BINDIR\""
-for NAME in isabelle isabelle-process isabelle_scala_script
+for NAME in isabelle isabelle_process isabelle_scala_script
do
BIN="$BINDIR/$NAME"
DIST="$DISTDIR/bin/$NAME"
--- a/lib/scripts/getsettings Sun Apr 06 17:18:57 2014 +0200
+++ b/lib/scripts/getsettings Sun Apr 06 17:19:08 2014 +0200
@@ -44,14 +44,24 @@
export ISABELLE_HOME
#key executables
-ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle-process"
ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
+ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle_process"
function isabelle ()
{
"$ISABELLE_TOOL" "$@"
}
+function isabelle_process ()
+{
+ "$ISABELLE_PROCESS" "$@"
+}
+
+function isabelle_scala_script ()
+{
+ "$ISABELLE_HOME/bin/isabelle_scala_script" "$@"
+}
+
#platform
source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
if [ -z "$ISABELLE_PLATFORM" ]; then
--- a/src/Doc/System/Basics.thy Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Doc/System/Basics.thy Sun Apr 06 17:19:08 2014 +0200
@@ -22,7 +22,7 @@
and user interfaces).
\item The raw \emph{Isabelle process} (@{executable_ref
- "isabelle-process"}) runs logic sessions either interactively or in
+ "isabelle_process"}) runs logic sessions either interactively or in
batch mode. In particular, this view abstracts over the invocation
of the actual ML system to be used. Regular users rarely need to
care about the low-level process.
@@ -122,7 +122,7 @@
\item @{setting_def ISABELLE_PROCESS} and @{setting_def ISABELLE_TOOL} are set
automatically to the absolute path names of the @{executable
- "isabelle-process"} and @{executable isabelle} executables,
+ "isabelle_process"} and @{executable isabelle} executables,
respectively.
\item @{setting_ref ISABELLE_OUTPUT} will have the identifiers of
@@ -193,7 +193,7 @@
\item[@{setting_def ISABELLE_PROCESS}@{text "\<^sup>*"}, @{setting
ISABELLE_TOOL}@{text "\<^sup>*"}] are automatically set to the full path
- names of the @{executable "isabelle-process"} and @{executable
+ names of the @{executable "isabelle_process"} and @{executable
isabelle} executables, respectively. Thus other tools and scripts
need not assume that the @{file "$ISABELLE_HOME/bin"} directory is
on the current search path of the shell.
@@ -271,7 +271,7 @@
for displaying @{verbatim dvi} files.
\item[@{setting_def ISABELLE_TMP_PREFIX}@{text "\<^sup>*"}] is the
- prefix from which any running @{executable "isabelle-process"}
+ prefix from which any running @{executable "isabelle_process"}
derives an individual directory for temporary files. The default is
somewhere in @{file_unchecked "/tmp"}.
@@ -353,13 +353,13 @@
section {* The raw Isabelle process *}
text {*
- The @{executable_def "isabelle-process"} executable runs bare-bones
+ The @{executable_def "isabelle_process"} executable runs bare-bones
Isabelle logic sessions --- either interactively or in batch mode.
It provides an abstraction over the underlying ML system, and over
the actual heap file locations. Its usage is:
\begin{ttbox}
-Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT]
+Usage: isabelle_process [OPTIONS] [INPUT] [OUTPUT]
Options are:
-I startup Isar interaction mode
@@ -455,7 +455,7 @@
Run an interactive session of the default object-logic (as specified
by the @{setting ISABELLE_LOGIC} setting) like this:
\begin{ttbox}
-isabelle-process
+isabelle_process
\end{ttbox}
Usually @{setting ISABELLE_LOGIC} refers to one of the standard
@@ -464,7 +464,7 @@
directory specified by the @{setting ISABELLE_OUTPUT} setting) ---
may be invoked as follows:
\begin{ttbox}
-isabelle-process HOL Test
+isabelle_process HOL Test
\end{ttbox}
Ending this session normally (e.g.\ by typing control-D) dumps the
whole ML system state into @{verbatim Test} (be prepared for more
@@ -473,11 +473,11 @@
The @{verbatim Test} session may be continued later (still in
writable state) by:
\begin{ttbox}
-isabelle-process Test
+isabelle_process Test
\end{ttbox}
A read-only @{verbatim Test} session may be started by:
\begin{ttbox}
-isabelle-process -r Test
+isabelle_process -r Test
\end{ttbox}
\bigskip The next example demonstrates batch execution of Isabelle.
@@ -485,7 +485,7 @@
within ML (observe the delicate quoting rules for the Bash shell
vs.\ ML):
\begin{ttbox}
-isabelle-process -e 'Thy_Info.get_theory "Main";' -q -r HOL
+isabelle_process -e 'Thy_Info.get_theory "Main";' -q -r HOL
\end{ttbox}
Note that the output text will be interspersed with additional junk
messages by the ML runtime environment. The @{verbatim "-W"} option
--- a/src/Doc/System/Misc.thy Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Doc/System/Misc.thy Sun Apr 06 17:19:08 2014 +0200
@@ -200,7 +200,7 @@
distribution directory as determined by @{setting ISABELLE_HOME}.
The @{text BINDIR} argument tells where executable wrapper scripts
- for @{executable "isabelle-process"} and @{executable isabelle}
+ for @{executable "isabelle_process"} and @{executable isabelle}
should be placed, which is typically a directory in the shell's
@{setting PATH}, such as @{verbatim "$HOME/bin"}.
--- a/src/Doc/System/Presentation.thy Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Doc/System/Presentation.thy Sun Apr 06 17:19:08 2014 +0200
@@ -15,7 +15,7 @@
The tools @{tool_ref mkroot} and @{tool_ref build} provide the
primary means for managing Isabelle sessions, including proper setup
for presentation; @{tool build} takes care to have @{executable_ref
- "isabelle-process"} run any additional stages required for document
+ "isabelle_process"} run any additional stages required for document
preparation, notably the @{tool_ref document} and @{tool_ref latex}.
The complete tool chain for managing batch-mode Isabelle sessions is
illustrated in \figref{fig:session-tools}.
@@ -31,7 +31,7 @@
@{tool_ref build} & invoked repeatedly by the user to keep
session output up-to-date (HTML, documents etc.); \\
- @{executable "isabelle-process"} & run through @{tool_ref
+ @{executable "isabelle_process"} & run through @{tool_ref
build}; \\
@{tool_ref document} & run by the Isabelle process if document
--- a/src/Pure/General/name_space.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/General/name_space.ML Sun Apr 06 17:19:08 2014 +0200
@@ -189,13 +189,13 @@
(* extern *)
-val names_long_raw = Config.declare_option "names_long";
+val names_long_raw = Config.declare_option ("names_long", @{here});
val names_long = Config.bool names_long_raw;
-val names_short_raw = Config.declare_option "names_short";
+val names_short_raw = Config.declare_option ("names_short", @{here});
val names_short = Config.bool names_short_raw;
-val names_unique_raw = Config.declare_option "names_unique";
+val names_unique_raw = Config.declare_option ("names_unique", @{here});
val names_unique = Config.bool names_unique_raw;
fun extern ctxt space name =
--- a/src/Pure/General/position.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/General/position.ML Sun Apr 06 17:19:08 2014 +0200
@@ -20,8 +20,9 @@
val file_name: string -> Properties.T
val file_only: string -> T
val file: string -> T
+ val line_file_only: int -> string -> T
+ val line_file: int -> string -> T
val line: int -> T
- val line_file: int -> string -> T
val id: string -> T
val id_only: string -> T
val get_id: T -> string option
@@ -117,6 +118,7 @@
fun file_only name = Pos ((0, 0, 0), file_name name);
fun file name = Pos ((1, 1, 0), file_name name);
+fun line_file_only i name = Pos ((i, 0, 0), file_name name);
fun line_file i name = Pos ((i, 1, 0), file_name name);
fun line i = line_file i "";
--- a/src/Pure/General/secure.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/General/secure.ML Sun Apr 06 17:19:08 2014 +0200
@@ -58,15 +58,3 @@
end;
-(*override previous toplevel bindings!*)
-val use_text = Secure.use_text;
-val use_file = Secure.use_file;
-
-fun use s =
- Position.setmp_thread_data (Position.file_only s)
- (fn () =>
- Secure.use_file ML_Parse.global_context true s
- handle ERROR msg => (writeln msg; error "ML error")) ();
-
-val toplevel_pp = Secure.toplevel_pp;
-
--- a/src/Pure/Isar/attrib.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/Isar/attrib.ML Sun Apr 06 17:19:08 2014 +0200
@@ -58,14 +58,14 @@
val setup_config_int: Binding.binding -> (Context.generic -> int) -> int Config.T
val setup_config_real: Binding.binding -> (Context.generic -> real) -> real Config.T
val setup_config_string: Binding.binding -> (Context.generic -> string) -> string Config.T
- val option_bool: string -> bool Config.T * (theory -> theory)
- val option_int: string -> int Config.T * (theory -> theory)
- val option_real: string -> real Config.T * (theory -> theory)
- val option_string: string -> string Config.T * (theory -> theory)
- val setup_option_bool: string -> bool Config.T
- val setup_option_int: string -> int Config.T
- val setup_option_real: string -> real Config.T
- val setup_option_string: string -> string Config.T
+ val option_bool: string * Position.T -> bool Config.T * (theory -> theory)
+ val option_int: string * Position.T -> int Config.T * (theory -> theory)
+ val option_real: string * Position.T -> real Config.T * (theory -> theory)
+ val option_string: string * Position.T -> string Config.T * (theory -> theory)
+ val setup_option_bool: string * Position.T -> bool Config.T
+ val setup_option_int: string * Position.T -> int Config.T
+ val setup_option_real: string * Position.T -> real Config.T
+ val setup_option_string: string * Position.T -> string Config.T
end;
structure Attrib: ATTRIB =
@@ -190,7 +190,8 @@
fun internal att = Args.src ("Pure.attribute", Position.none) [Token.mk_attribute att];
val _ = Theory.setup
- (setup (Binding.name "attribute") (Scan.lift Args.internal_attribute >> Morphism.form)
+ (setup (Binding.make ("attribute", @{here}))
+ (Scan.lift Args.internal_attribute >> Morphism.form)
"internal attribute");
@@ -373,13 +374,15 @@
fun declare make coerce binding default =
let
val name = Binding.name_of binding;
- val config_value = Config.declare name (make o default);
+ val pos = Binding.pos_of binding;
+ val config_value = Config.declare (name, pos) (make o default);
val config = coerce config_value;
in (config, register binding config_value) end;
in
-fun register_config config = register (Binding.name (Config.name_of config)) config;
+fun register_config config =
+ register (Binding.make (Config.name_of config, Config.pos_of config)) config;
val config_bool = declare Config.Bool Config.bool;
val config_int = declare Config.Int Config.int;
@@ -413,14 +416,14 @@
local
-fun declare_option coerce name =
+fun declare_option coerce (name, pos) =
let
- val config = Config.declare_option name;
+ val config = Config.declare_option (name, pos);
in (coerce config, register_config config) end;
-fun setup_option coerce name =
+fun setup_option coerce (name, pos) =
let
- val config = Config.declare_option name;
+ val config = Config.declare_option (name, pos);
val _ = Theory.setup (register_config config);
in coerce config end;
--- a/src/Pure/Isar/proof_context.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/Isar/proof_context.ML Sun Apr 06 17:19:08 2014 +0200
@@ -572,7 +572,7 @@
end;
-val show_abbrevs_raw = Config.declare "show_abbrevs" (fn _ => Config.Bool true);
+val show_abbrevs_raw = Config.declare ("show_abbrevs", @{here}) (fn _ => Config.Bool true);
val show_abbrevs = Config.bool show_abbrevs_raw;
fun contract_abbrevs ctxt t =
@@ -605,7 +605,8 @@
local
-val dummies = Config.bool (Config.declare "Proof_Context.dummies" (K (Config.Bool false)));
+val dummies =
+ Config.bool (Config.declare ("Proof_Context.dummies", @{here}) (K (Config.Bool false)));
fun check_dummies ctxt t =
if Config.get ctxt dummies then t
@@ -1338,8 +1339,11 @@
(* core context *)
-val debug = Config.bool (Config.declare "Proof_Context.debug" (K (Config.Bool false)));
-val verbose = Config.bool (Config.declare "Proof_Context.verbose" (K (Config.Bool false)));
+val debug =
+ Config.bool (Config.declare ("Proof_Context.debug", @{here}) (K (Config.Bool false)));
+
+val verbose =
+ Config.bool (Config.declare ("Proof_Context.verbose", @{here}) (K (Config.Bool false)));
fun pretty_ctxt ctxt =
if not (Config.get ctxt debug) then []
--- a/src/Pure/ML-Systems/compiler_polyml.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/ML-Systems/compiler_polyml.ML Sun Apr 06 17:19:08 2014 +0200
@@ -15,7 +15,8 @@
(start_line, name) verbose txt =
let
val line = Unsynchronized.ref start_line;
- val in_buffer = Unsynchronized.ref (String.explode (tune_source txt));
+ val in_buffer =
+ Unsynchronized.ref (String.explode (tune_source (ml_positions start_line name txt)));
val out_buffer = Unsynchronized.ref ([]: string list);
fun output () = drop_newline (implode (rev (! out_buffer)));
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_positions.ML Sun Apr 06 17:19:08 2014 +0200
@@ -0,0 +1,16 @@
+(* Title: Pure/ML-Systems/ml_positions.ML
+ Author: Makarius
+
+Approximate ML antiquotation @{here} for Isabelle/Pure bootstrap.
+*)
+
+fun ml_positions start_line name txt =
+ let
+ fun positions line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res =
+ let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")"
+ in positions line cs (s :: res) end
+ | positions line (c :: cs) res =
+ positions (if c = #"\n" then line + 1 else line) cs (str c :: res)
+ | positions _ [] res = rev res;
+ in String.concat (positions start_line (String.explode txt) []) end;
+
--- a/src/Pure/ML-Systems/polyml.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/ML-Systems/polyml.ML Sun Apr 06 17:19:08 2014 +0200
@@ -113,6 +113,7 @@
(* ML compiler *)
use "ML-Systems/use_context.ML";
+use "ML-Systems/ml_positions.ML";
use "ML-Systems/compiler_polyml.ML";
PolyML.Compiler.reportUnreferencedIds := true;
--- a/src/Pure/ML-Systems/smlnj.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML Sun Apr 06 17:19:08 2014 +0200
@@ -20,6 +20,7 @@
structure PolyML = struct end;
use "ML-Systems/pp_dummy.ML";
use "ML-Systems/use_context.ML";
+use "ML-Systems/ml_positions.ML";
val seconds = Time.fromReal;
@@ -91,9 +92,10 @@
in String.substring (str, 0, Int.max (0, size str - 1)) end;
in
Control.Print.out := out;
- Backend.Interact.useStream (TextIO.openString (tune_source txt)) handle exn =>
- (Control.Print.out := out_orig;
- error ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
+ Backend.Interact.useStream (TextIO.openString (tune_source (ml_positions line name txt)))
+ handle exn =>
+ (Control.Print.out := out_orig;
+ error ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
Control.Print.out := out_orig;
if verbose then print (output ()) else ()
end;
--- a/src/Pure/ML/ml_antiquotation.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/ML/ml_antiquotation.ML Sun Apr 06 17:19:08 2014 +0200
@@ -58,7 +58,7 @@
(* basic antiquotations *)
val _ = Theory.setup
- (declaration (Binding.name "here") (Scan.succeed ())
+ (declaration (Binding.make ("here", @{here})) (Scan.succeed ())
(fn src => fn () => fn ctxt =>
let
val (a, ctxt') = variant "position" ctxt;
@@ -67,7 +67,7 @@
val body = "Isabelle." ^ a;
in (K (env, body), ctxt') end) #>
- value (Binding.name "binding")
+ value (Binding.make ("binding", @{here}))
(Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding));
end;
--- a/src/Pure/ML/ml_context.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/ML/ml_context.ML Sun Apr 06 17:19:08 2014 +0200
@@ -188,7 +188,3 @@
end;
-fun use s =
- ML_Context.eval_file (ML_Compiler.verbose true ML_Compiler.flags) (Path.explode s)
- handle ERROR msg => (writeln msg; error "ML error");
-
--- a/src/Pure/ML/ml_options.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/ML/ml_options.ML Sun Apr 06 17:19:08 2014 +0200
@@ -21,13 +21,14 @@
(* source trace *)
-val source_trace_raw = Config.declare "ML_source_trace" (fn _ => Config.Bool false);
+val source_trace_raw =
+ Config.declare ("ML_source_trace", @{here}) (fn _ => Config.Bool false);
val source_trace = Config.bool source_trace_raw;
(* exception trace *)
-val exception_trace_raw = Config.declare_option "ML_exception_trace";
+val exception_trace_raw = Config.declare_option ("ML_exception_trace", @{here});
val exception_trace = Config.bool exception_trace_raw;
fun exception_trace_enabled NONE =
@@ -38,7 +39,7 @@
(* print depth *)
val print_depth_raw =
- Config.declare "ML_print_depth" (fn _ => Config.Int (get_default_print_depth ()));
+ Config.declare ("ML_print_depth", @{here}) (fn _ => Config.Int (get_default_print_depth ()));
val print_depth = Config.int print_depth_raw;
fun get_print_depth () =
--- a/src/Pure/Proof/extraction.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/Proof/extraction.ML Sun Apr 06 17:19:08 2014 +0200
@@ -36,12 +36,14 @@
val add_syntax =
Sign.root_path
- #> Sign.add_types_global [(Binding.name "Type", 0, NoSyn), (Binding.name "Null", 0, NoSyn)]
+ #> Sign.add_types_global
+ [(Binding.make ("Type", @{here}), 0, NoSyn),
+ (Binding.make ("Null", @{here}), 0, NoSyn)]
#> Sign.add_consts
- [(Binding.name "typeof", typ "'b => Type", NoSyn),
- (Binding.name "Type", typ "'a itself => Type", NoSyn),
- (Binding.name "Null", typ "Null", NoSyn),
- (Binding.name "realizes", typ "'a => 'b => 'b", NoSyn)];
+ [(Binding.make ("typeof", @{here}), typ "'b => Type", NoSyn),
+ (Binding.make ("Type", @{here}), typ "'a itself => Type", NoSyn),
+ (Binding.make ("Null", @{here}), typ "Null", NoSyn),
+ (Binding.make ("realizes", @{here}), typ "'a => 'b => 'b", NoSyn)];
val nullT = Type ("Null", []);
val nullt = Const ("Null", nullT);
--- a/src/Pure/Proof/proof_syntax.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Sun Apr 06 17:19:08 2014 +0200
@@ -43,44 +43,47 @@
thy
|> Sign.root_path
|> Sign.set_defsort []
- |> Sign.add_types_global [(Binding.name "proof", 0, NoSyn)]
+ |> Sign.add_types_global
+ [(Binding.make ("proof", @{here}), 0, NoSyn)]
|> fold (snd oo Sign.declare_const_global)
- [((Binding.name "Appt", [proofT, aT] ---> proofT), Mixfix ("(1_ %/ _)", [4, 5], 4)),
- ((Binding.name "AppP", [proofT, proofT] ---> proofT), Mixfix ("(1_ %%/ _)", [4, 5], 4)),
- ((Binding.name "Abst", (aT --> proofT) --> proofT), NoSyn),
- ((Binding.name "AbsP", [propT, proofT --> proofT] ---> proofT), NoSyn),
- ((Binding.name "Hyp", propT --> proofT), NoSyn),
- ((Binding.name "Oracle", propT --> proofT), NoSyn),
- ((Binding.name "OfClass", (Term.a_itselfT --> propT) --> proofT), NoSyn),
- ((Binding.name "MinProof", proofT), Delimfix "?")]
- |> Sign.add_nonterminals_global [Binding.name "param", Binding.name "params"]
+ [((Binding.make ("Appt", @{here}), [proofT, aT] ---> proofT), Mixfix ("(1_ %/ _)", [4, 5], 4)),
+ ((Binding.make ("AppP", @{here}), [proofT, proofT] ---> proofT), Mixfix ("(1_ %%/ _)", [4, 5], 4)),
+ ((Binding.make ("Abst", @{here}), (aT --> proofT) --> proofT), NoSyn),
+ ((Binding.make ("AbsP", @{here}), [propT, proofT --> proofT] ---> proofT), NoSyn),
+ ((Binding.make ("Hyp", @{here}), propT --> proofT), NoSyn),
+ ((Binding.make ("Oracle", @{here}), propT --> proofT), NoSyn),
+ ((Binding.make ("OfClass", @{here}), (Term.a_itselfT --> propT) --> proofT), NoSyn),
+ ((Binding.make ("MinProof", @{here}), proofT), Delimfix "?")]
+ |> Sign.add_nonterminals_global
+ [Binding.make ("param", @{here}),
+ Binding.make ("params", @{here})]
|> Sign.add_syntax Syntax.mode_default
- [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
- ("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
- ("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
- ("_Lam1", [idtT, propT] ---> paramT, Mixfix ("_: _", [0, 0], 0)),
- ("", paramT --> paramT, Delimfix "'(_')"),
- ("", idtT --> paramsT, Delimfix "_"),
- ("", paramT --> paramsT, Delimfix "_")]
+ [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
+ ("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
+ ("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
+ ("_Lam1", [idtT, propT] ---> paramT, Mixfix ("_: _", [0, 0], 0)),
+ ("", paramT --> paramT, Delimfix "'(_')"),
+ ("", idtT --> paramsT, Delimfix "_"),
+ ("", paramT --> paramsT, Delimfix "_")]
|> Sign.add_syntax (Symbol.xsymbolsN, true)
- [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)),
- (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
- (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \<bullet>/ _)", [4, 5], 4))]
+ [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)),
+ (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
+ (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \<bullet>/ _)", [4, 5], 4))]
|> Sign.add_trrules (map Syntax.Parse_Print_Rule
- [(Ast.mk_appl (Ast.Constant "_Lam")
- [Ast.mk_appl (Ast.Constant "_Lam0")
- [Ast.Variable "l", Ast.Variable "m"], Ast.Variable "A"],
- Ast.mk_appl (Ast.Constant "_Lam")
- [Ast.Variable "l",
- Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "m", Ast.Variable "A"]]),
- (Ast.mk_appl (Ast.Constant "_Lam")
- [Ast.mk_appl (Ast.Constant "_Lam1")
- [Ast.Variable "x", Ast.Variable "A"], Ast.Variable "B"],
- Ast.mk_appl (Ast.Constant (Lexicon.mark_const "AbsP")) [Ast.Variable "A",
- (Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "B"])]),
- (Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "x", Ast.Variable "A"],
- Ast.mk_appl (Ast.Constant (Lexicon.mark_const "Abst"))
- [(Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "A"])])]);
+ [(Ast.mk_appl (Ast.Constant "_Lam")
+ [Ast.mk_appl (Ast.Constant "_Lam0")
+ [Ast.Variable "l", Ast.Variable "m"], Ast.Variable "A"],
+ Ast.mk_appl (Ast.Constant "_Lam")
+ [Ast.Variable "l",
+ Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "m", Ast.Variable "A"]]),
+ (Ast.mk_appl (Ast.Constant "_Lam")
+ [Ast.mk_appl (Ast.Constant "_Lam1")
+ [Ast.Variable "x", Ast.Variable "A"], Ast.Variable "B"],
+ Ast.mk_appl (Ast.Constant (Lexicon.mark_const "AbsP")) [Ast.Variable "A",
+ (Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "B"])]),
+ (Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "x", Ast.Variable "A"],
+ Ast.mk_appl (Ast.Constant (Lexicon.mark_const "Abst"))
+ [(Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "A"])])]);
(**** translation between proof terms and pure terms ****)
--- a/src/Pure/ROOT Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/ROOT Sun Apr 06 17:19:08 2014 +0200
@@ -6,6 +6,7 @@
"General/exn.ML"
"ML-Systems/compiler_polyml.ML"
"ML-Systems/ml_name_space.ML"
+ "ML-Systems/ml_positions.ML"
"ML-Systems/ml_pretty.ML"
"ML-Systems/ml_system.ML"
"ML-Systems/multithreading.ML"
@@ -30,6 +31,7 @@
"General/exn.ML"
"ML-Systems/compiler_polyml.ML"
"ML-Systems/ml_name_space.ML"
+ "ML-Systems/ml_positions.ML"
"ML-Systems/ml_pretty.ML"
"ML-Systems/ml_system.ML"
"ML-Systems/multithreading.ML"
--- a/src/Pure/ROOT.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/ROOT.ML Sun Apr 06 17:19:08 2014 +0200
@@ -38,6 +38,16 @@
use "ML/ml_parse.ML";
use "General/secure.ML";
+val use_text = Secure.use_text;
+val use_file = Secure.use_file;
+
+fun use s =
+ Position.setmp_thread_data (Position.file_only s)
+ (fn () =>
+ Secure.use_file ML_Parse.global_context true s
+ handle ERROR msg => (writeln msg; error "ML error")) ();
+
+val toplevel_pp = Secure.toplevel_pp;
(** bootstrap phase 1: towards ML within Isar context *)
@@ -131,9 +141,6 @@
use "context_position.ML";
use "config.ML";
-val quick_and_dirty_raw = Config.declare_option "quick_and_dirty";
-val quick_and_dirty = Config.bool quick_and_dirty_raw;
-
(* inner syntax *)
@@ -236,6 +243,10 @@
use "ML/ml_context.ML";
use "ML/ml_antiquotation.ML";
+fun use s =
+ ML_Context.eval_file (ML_Compiler.verbose true ML_Compiler.flags) (Path.explode s)
+ handle ERROR msg => (writeln msg; error "ML error");
+
(** bootstrap phase 2: towards Pure.thy and final ML toplevel setup *)
--- a/src/Pure/Syntax/ast.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/Syntax/ast.ML Sun Apr 06 17:19:08 2014 +0200
@@ -164,10 +164,10 @@
(* normalize *)
-val trace_raw = Config.declare "syntax_ast_trace" (fn _ => Config.Bool false);
+val trace_raw = Config.declare ("syntax_ast_trace", @{here}) (fn _ => Config.Bool false);
val trace = Config.bool trace_raw;
-val stats_raw = Config.declare "syntax_ast_stats" (fn _ => Config.Bool false);
+val stats_raw = Config.declare ("syntax_ast_stats", @{here}) (fn _ => Config.Bool false);
val stats = Config.bool stats_raw;
fun message head body =
--- a/src/Pure/Syntax/parser.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/Syntax/parser.ML Sun Apr 06 17:19:08 2014 +0200
@@ -626,7 +626,8 @@
(*trigger value for warnings*)
-val branching_level = Config.int (Config.declare "syntax_branching_level" (fn _ => Config.Int 600));
+val branching_level =
+ Config.int (Config.declare ("syntax_branching_level", @{here}) (fn _ => Config.Int 600));
(*get all productions of a NT and NTs chained to it which can
be started by specified token*)
--- a/src/Pure/Syntax/printer.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/Syntax/printer.ML Sun Apr 06 17:19:08 2014 +0200
@@ -48,27 +48,29 @@
(** options for printing **)
-val show_brackets_raw = Config.declare_option "show_brackets";
+val show_brackets_raw = Config.declare_option ("show_brackets", @{here});
val show_brackets = Config.bool show_brackets_raw;
-val show_types_raw = Config.declare_option "show_types";
+val show_types_raw = Config.declare_option ("show_types", @{here});
val show_types = Config.bool show_types_raw;
-val show_sorts_raw = Config.declare_option "show_sorts";
+val show_sorts_raw = Config.declare_option ("show_sorts", @{here});
val show_sorts = Config.bool show_sorts_raw;
val show_markup_default = Unsynchronized.ref false;
-val show_markup_raw = Config.declare "show_markup" (fn _ => Config.Bool (! show_markup_default));
+val show_markup_raw =
+ Config.declare ("show_markup", @{here}) (fn _ => Config.Bool (! show_markup_default));
val show_markup = Config.bool show_markup_raw;
-val show_structs_raw = Config.declare "show_structs" (fn _ => Config.Bool false);
+val show_structs_raw =
+ Config.declare ("show_structs", @{here}) (fn _ => Config.Bool false);
val show_structs = Config.bool show_structs_raw;
-val show_question_marks_raw = Config.declare_option "show_question_marks";
+val show_question_marks_raw = Config.declare_option ("show_question_marks", @{here});
val show_question_marks = Config.bool show_question_marks_raw;
val show_type_emphasis =
- Config.bool (Config.declare "show_type_emphasis" (fn _ => Config.Bool true));
+ Config.bool (Config.declare ("show_type_emphasis", @{here}) (fn _ => Config.Bool true));
fun type_emphasis ctxt T =
T <> dummyT andalso
@@ -166,7 +168,8 @@
| is_chain [Arg _] = true
| is_chain _ = false;
-val pretty_priority = Config.int (Config.declare "Syntax.pretty_priority" (K (Config.Int 0)));
+val pretty_priority =
+ Config.int (Config.declare ("Syntax.pretty_priority", @{here}) (K (Config.Int 0)));
fun pretty type_mode curried ctxt tabs trf markup_trans markup_extern ast0 =
let
--- a/src/Pure/Syntax/syntax.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/Syntax/syntax.ML Sun Apr 06 17:19:08 2014 +0200
@@ -148,12 +148,14 @@
(* configuration options *)
-val root = Config.string (Config.declare "syntax_root" (K (Config.String "any")));
+val root = Config.string (Config.declare ("syntax_root", @{here}) (K (Config.String "any")));
-val ambiguity_warning_raw = Config.declare "syntax_ambiguity_warning" (fn _ => Config.Bool true);
+val ambiguity_warning_raw =
+ Config.declare ("syntax_ambiguity_warning", @{here}) (fn _ => Config.Bool true);
val ambiguity_warning = Config.bool ambiguity_warning_raw;
-val ambiguity_limit_raw = Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10);
+val ambiguity_limit_raw =
+ Config.declare ("syntax_ambiguity_limit", @{here}) (fn _ => Config.Int 10);
val ambiguity_limit = Config.int ambiguity_limit_raw;
@@ -305,7 +307,8 @@
(* global pretty printing *)
-val pretty_global = Config.bool (Config.declare "Syntax.pretty_global" (K (Config.Bool false)));
+val pretty_global =
+ Config.bool (Config.declare ("Syntax.pretty_global", @{here}) (K (Config.Bool false)));
fun is_pretty_global ctxt = Config.get ctxt pretty_global;
val set_pretty_global = Config.put pretty_global;
val init_pretty_global = set_pretty_global true o Proof_Context.init_global;
--- a/src/Pure/Syntax/syntax_trans.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML Sun Apr 06 17:19:08 2014 +0200
@@ -295,7 +295,7 @@
| t' => Abs (a, T, t'))
| eta_abs t = t;
-val eta_contract_raw = Config.declare_option "eta_contract";
+val eta_contract_raw = Config.declare_option ("eta_contract", @{here});
val eta_contract = Config.bool eta_contract_raw;
fun eta_contr ctxt tm =
--- a/src/Pure/Thy/thy_output.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/Thy/thy_output.ML Sun Apr 06 17:19:08 2014 +0200
@@ -43,12 +43,12 @@
(** options **)
-val display = Attrib.setup_option_bool "thy_output_display";
-val break = Attrib.setup_option_bool "thy_output_break";
-val quotes = Attrib.setup_option_bool "thy_output_quotes";
-val indent = Attrib.setup_option_int "thy_output_indent";
-val source = Attrib.setup_option_bool "thy_output_source";
-val modes = Attrib.setup_option_string "thy_output_modes";
+val display = Attrib.setup_option_bool ("thy_output_display", @{here});
+val break = Attrib.setup_option_bool ("thy_output_break", @{here});
+val quotes = Attrib.setup_option_bool ("thy_output_quotes", @{here});
+val indent = Attrib.setup_option_int ("thy_output_indent", @{here});
+val source = Attrib.setup_option_bool ("thy_output_source", @{here});
+val modes = Attrib.setup_option_string ("thy_output_modes", @{here});
structure Wrappers = Proof_Data
--- a/src/Pure/config.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/config.ML Sun Apr 06 17:19:08 2014 +0200
@@ -24,11 +24,12 @@
val get_generic: Context.generic -> 'a T -> 'a
val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
- val declare: string -> (Context.generic -> value) -> raw
- val declare_global: string -> (Context.generic -> value) -> raw
- val declare_option: string -> raw
- val declare_option_global: string -> raw
+ val declare: string * Position.T -> (Context.generic -> value) -> raw
+ val declare_global: string * Position.T -> (Context.generic -> value) -> raw
+ val declare_option: string * Position.T -> raw
+ val declare_option_global: string * Position.T -> raw
val name_of: 'a T -> string
+ val pos_of: 'a T -> Position.T
end;
structure Config: CONFIG =
@@ -59,11 +60,11 @@
| same_type (String _) (String _) = true
| same_type _ _ = false;
-fun type_check name f value =
+fun type_check (name, pos) f value =
let
val value' = f value;
val _ = same_type value value' orelse
- error ("Ill-typed configuration option " ^ quote name ^ ": " ^
+ error ("Ill-typed configuration option " ^ quote name ^ Position.here pos ^ ": " ^
print_type value ^ " expected,\nbut " ^ print_type value' ^ " was found");
in value' end;
@@ -72,13 +73,15 @@
datatype 'a T = Config of
{name: string,
+ pos: Position.T,
get_value: Context.generic -> 'a,
map_value: ('a -> 'a) -> Context.generic -> Context.generic};
type raw = value T;
-fun coerce make dest (Config {name, get_value, map_value}) = Config
+fun coerce make dest (Config {name, pos, get_value, map_value}) = Config
{name = name,
+ pos = pos,
get_value = dest o get_value,
map_value = fn f => map_value (make o f o dest)};
@@ -112,7 +115,7 @@
local
-fun declare_generic global name default =
+fun declare_generic global (name, pos) default =
let
val id = serial ();
@@ -122,7 +125,7 @@
| NONE => default context);
fun update_value f context =
- Value.map (Inttab.update (id, type_check name f (get_value context))) context;
+ Value.map (Inttab.update (id, type_check (name, pos) f (get_value context))) context;
fun map_value f (context as Context.Proof ctxt) =
let val context' = update_value f context in
@@ -137,9 +140,9 @@
else context'
end
| map_value f context = update_value f context;
- in Config {name = name, get_value = get_value, map_value = map_value} end;
+ in Config {name = name, pos = pos, get_value = get_value, map_value = map_value} end;
-fun declare_option_generic global name =
+fun declare_option_generic global (name, pos) =
let
val typ = Options.default_typ name;
val default =
@@ -147,8 +150,8 @@
else if typ = Options.intT then fn _ => Int (Options.default_int name)
else if typ = Options.realT then fn _ => Real (Options.default_real name)
else if typ = Options.stringT then fn _ => String (Options.default_string name)
- else error ("Unknown type for option " ^ quote name ^ " : " ^ quote typ);
- in declare_generic global name default end;
+ else error ("Unknown type for option " ^ quote name ^ Position.here pos ^ " : " ^ quote typ);
+ in declare_generic global (name, pos) default end;
in
@@ -160,6 +163,7 @@
end;
fun name_of (Config {name, ...}) = name;
+fun pos_of (Config {pos, ...}) = pos;
(*final declarations of this structure!*)
--- a/src/Pure/conjunction.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/conjunction.ML Sun Apr 06 17:19:08 2014 +0200
@@ -84,11 +84,14 @@
in
-val conjunctionD1 = Drule.store_standard_thm (Binding.name "conjunctionD1") (conjunctionD #1);
-val conjunctionD2 = Drule.store_standard_thm (Binding.name "conjunctionD2") (conjunctionD #2);
+val conjunctionD1 =
+ Drule.store_standard_thm (Binding.make ("conjunctionD1", @{here})) (conjunctionD #1);
+
+val conjunctionD2 =
+ Drule.store_standard_thm (Binding.make ("conjunctionD2", @{here})) (conjunctionD #2);
val conjunctionI =
- Drule.store_standard_thm (Binding.name "conjunctionI")
+ Drule.store_standard_thm (Binding.make ("conjunctionI", @{here}))
(Drule.implies_intr_list [A, B]
(Thm.equal_elim
(Thm.symmetric conjunction_def)
--- a/src/Pure/display.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/display.ML Sun Apr 06 17:19:08 2014 +0200
@@ -35,10 +35,10 @@
val show_consts = Goal_Display.show_consts;
-val show_hyps_raw = Config.declare "show_hyps" (fn _ => Config.Bool false);
+val show_hyps_raw = Config.declare ("show_hyps", @{here}) (fn _ => Config.Bool false);
val show_hyps = Config.bool show_hyps_raw;
-val show_tags_raw = Config.declare "show_tags" (fn _ => Config.Bool false);
+val show_tags_raw = Config.declare ("show_tags", @{here}) (fn _ => Config.Bool false);
val show_tags = Config.bool show_tags_raw;
--- a/src/Pure/drule.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/drule.ML Sun Apr 06 17:19:08 2014 +0200
@@ -385,13 +385,13 @@
val reflexive_thm =
let val cx = certify (Var(("x",0),TVar(("'a",0),[])))
- in store_standard_thm_open (Binding.name "reflexive") (Thm.reflexive cx) end;
+ in store_standard_thm_open (Binding.make ("reflexive", @{here})) (Thm.reflexive cx) end;
val symmetric_thm =
let
val xy = read_prop "x::'a == y::'a";
val thm = Thm.implies_intr xy (Thm.symmetric (Thm.assume xy));
- in store_standard_thm_open (Binding.name "symmetric") thm end;
+ in store_standard_thm_open (Binding.make ("symmetric", @{here})) thm end;
val transitive_thm =
let
@@ -400,7 +400,7 @@
val xythm = Thm.assume xy;
val yzthm = Thm.assume yz;
val thm = Thm.implies_intr yz (Thm.transitive xythm yzthm);
- in store_standard_thm_open (Binding.name "transitive") thm end;
+ in store_standard_thm_open (Binding.make ("transitive", @{here})) thm end;
fun extensional eq =
let val eq' =
@@ -408,7 +408,7 @@
in Thm.equal_elim (Thm.eta_conversion (cprop_of eq')) eq' end;
val equals_cong =
- store_standard_thm_open (Binding.name "equals_cong")
+ store_standard_thm_open (Binding.make ("equals_cong", @{here}))
(Thm.reflexive (read_prop "x::'a == y::'a"));
val imp_cong =
@@ -418,13 +418,14 @@
val AC = read_prop "A ==> C"
val A = read_prop "A"
in
- store_standard_thm_open (Binding.name "imp_cong") (Thm.implies_intr ABC (Thm.equal_intr
- (Thm.implies_intr AB (Thm.implies_intr A
- (Thm.equal_elim (Thm.implies_elim (Thm.assume ABC) (Thm.assume A))
- (Thm.implies_elim (Thm.assume AB) (Thm.assume A)))))
- (Thm.implies_intr AC (Thm.implies_intr A
- (Thm.equal_elim (Thm.symmetric (Thm.implies_elim (Thm.assume ABC) (Thm.assume A)))
- (Thm.implies_elim (Thm.assume AC) (Thm.assume A)))))))
+ store_standard_thm_open (Binding.make ("imp_cong", @{here}))
+ (Thm.implies_intr ABC (Thm.equal_intr
+ (Thm.implies_intr AB (Thm.implies_intr A
+ (Thm.equal_elim (Thm.implies_elim (Thm.assume ABC) (Thm.assume A))
+ (Thm.implies_elim (Thm.assume AB) (Thm.assume A)))))
+ (Thm.implies_intr AC (Thm.implies_intr A
+ (Thm.equal_elim (Thm.symmetric (Thm.implies_elim (Thm.assume ABC) (Thm.assume A)))
+ (Thm.implies_elim (Thm.assume AC) (Thm.assume A)))))))
end;
val swap_prems_eq =
@@ -434,7 +435,7 @@
val A = read_prop "A"
val B = read_prop "B"
in
- store_standard_thm_open (Binding.name "swap_prems_eq")
+ store_standard_thm_open (Binding.make ("swap_prems_eq", @{here}))
(Thm.equal_intr
(Thm.implies_intr ABC (Thm.implies_intr B (Thm.implies_intr A
(Thm.implies_elim (Thm.implies_elim (Thm.assume ABC) (Thm.assume A)) (Thm.assume B)))))
@@ -504,11 +505,13 @@
(*** Some useful meta-theorems ***)
(*The rule V/V, obtains assumption solving for eresolve_tac*)
-val asm_rl = store_standard_thm_open (Binding.name "asm_rl") (Thm.trivial (read_prop "?psi"));
+val asm_rl =
+ store_standard_thm_open (Binding.make ("asm_rl", @{here}))
+ (Thm.trivial (read_prop "?psi"));
(*Meta-level cut rule: [| V==>W; V |] ==> W *)
val cut_rl =
- store_standard_thm_open (Binding.name "cut_rl")
+ store_standard_thm_open (Binding.make ("cut_rl", @{here}))
(Thm.trivial (read_prop "?psi ==> ?theta"));
(*Generalized elim rule for one conclusion; cut_rl with reversed premises:
@@ -518,8 +521,9 @@
val V = read_prop "V";
val VW = read_prop "V ==> W";
in
- store_standard_thm_open (Binding.name "revcut_rl")
- (Thm.implies_intr V (Thm.implies_intr VW (Thm.implies_elim (Thm.assume VW) (Thm.assume V))))
+ store_standard_thm_open (Binding.make ("revcut_rl", @{here}))
+ (Thm.implies_intr V
+ (Thm.implies_intr VW (Thm.implies_elim (Thm.assume VW) (Thm.assume V))))
end;
(*for deleting an unwanted assumption*)
@@ -528,7 +532,7 @@
val V = read_prop "V";
val W = read_prop "W";
val thm = Thm.implies_intr V (Thm.implies_intr W (Thm.assume W));
- in store_standard_thm_open (Binding.name "thin_rl") thm end;
+ in store_standard_thm_open (Binding.make ("thin_rl", @{here})) thm end;
(* (!!x. PROP ?V) == PROP ?V Allows removal of redundant parameters*)
val triv_forall_equality =
@@ -537,7 +541,7 @@
val QV = read_prop "!!x::'a. V";
val x = certify (Free ("x", Term.aT []));
in
- store_standard_thm_open (Binding.name "triv_forall_equality")
+ store_standard_thm_open (Binding.make ("triv_forall_equality", @{here}))
(Thm.equal_intr (Thm.implies_intr QV (Thm.forall_elim x (Thm.assume QV)))
(Thm.implies_intr V (Thm.forall_intr x (Thm.assume V))))
end;
@@ -550,8 +554,9 @@
val AAB = read_prop "Phi ==> Phi ==> Psi";
val A = read_prop "Phi";
in
- store_standard_thm_open (Binding.name "distinct_prems_rl")
- (implies_intr_list [AAB, A] (implies_elim_list (Thm.assume AAB) [Thm.assume A, Thm.assume A]))
+ store_standard_thm_open (Binding.make ("distinct_prems_rl", @{here}))
+ (implies_intr_list [AAB, A]
+ (implies_elim_list (Thm.assume AAB) [Thm.assume A, Thm.assume A]))
end;
(* [| PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi |]
@@ -563,8 +568,9 @@
val PQ = read_prop "phi ==> psi";
val QP = read_prop "psi ==> phi";
in
- store_standard_thm_open (Binding.name "equal_intr_rule")
- (Thm.implies_intr PQ (Thm.implies_intr QP (Thm.equal_intr (Thm.assume PQ) (Thm.assume QP))))
+ store_standard_thm_open (Binding.make ("equal_intr_rule", @{here}))
+ (Thm.implies_intr PQ
+ (Thm.implies_intr QP (Thm.equal_intr (Thm.assume PQ) (Thm.assume QP))))
end;
(* PROP ?phi == PROP ?psi ==> PROP ?phi ==> PROP ?psi *)
@@ -573,13 +579,13 @@
val eq = read_prop "phi::prop == psi::prop";
val P = read_prop "phi";
in
- store_standard_thm_open (Binding.name "equal_elim_rule1")
+ store_standard_thm_open (Binding.make ("equal_elim_rule1", @{here}))
(Thm.equal_elim (Thm.assume eq) (Thm.assume P) |> implies_intr_list [eq, P])
end;
(* PROP ?psi == PROP ?phi ==> PROP ?phi ==> PROP ?psi *)
val equal_elim_rule2 =
- store_standard_thm_open (Binding.name "equal_elim_rule2")
+ store_standard_thm_open (Binding.make ("equal_elim_rule2", @{here}))
(symmetric_thm RS equal_elim_rule1);
(* PROP ?phi ==> PROP ?phi ==> PROP ?psi ==> PROP ?psi *)
@@ -588,7 +594,7 @@
val P = read_prop "phi";
val Q = read_prop "psi";
val thm = implies_intr_list [P, P, Q] (Thm.assume Q);
- in store_standard_thm_open (Binding.name "remdups_rl") thm end;
+ in store_standard_thm_open (Binding.make ("remdups_rl", @{here})) thm end;
@@ -610,15 +616,16 @@
val protect = Thm.apply (certify Logic.protectC);
val protectI =
- store_standard_thm (Binding.conceal (Binding.name "protectI"))
+ store_standard_thm (Binding.conceal (Binding.make ("protectI", @{here})))
(Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A));
val protectD =
- store_standard_thm (Binding.conceal (Binding.name "protectD"))
+ store_standard_thm (Binding.conceal (Binding.make ("protectD", @{here})))
(Thm.equal_elim prop_def (Thm.assume (protect A)));
val protect_cong =
- store_standard_thm_open (Binding.name "protect_cong") (Thm.reflexive (protect A));
+ store_standard_thm_open (Binding.make ("protect_cong", @{here}))
+ (Thm.reflexive (protect A));
fun implies_intr_protected asms th =
let val asms' = map protect asms in
@@ -632,7 +639,7 @@
(* term *)
val termI =
- store_standard_thm (Binding.conceal (Binding.name "termI"))
+ store_standard_thm (Binding.conceal (Binding.make ("termI", @{here})))
(Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A)));
fun mk_term ct =
@@ -660,11 +667,11 @@
(* sort_constraint *)
val sort_constraintI =
- store_standard_thm (Binding.conceal (Binding.name "sort_constraintI"))
+ store_standard_thm (Binding.conceal (Binding.make ("sort_constraintI", @{here})))
(Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T));
val sort_constraint_eq =
- store_standard_thm (Binding.conceal (Binding.name "sort_constraint_eq"))
+ store_standard_thm (Binding.conceal (Binding.make ("sort_constraint_eq", @{here})))
(Thm.equal_intr
(Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA)
(Thm.unvarify_global sort_constraintI)))
@@ -699,7 +706,7 @@
|> Thm.forall_intr cx
|> Thm.implies_intr cphi
|> Thm.implies_intr rhs)
- |> store_standard_thm_open (Binding.name "norm_hhf_eq")
+ |> store_standard_thm_open (Binding.make ("norm_hhf_eq", @{here}))
end;
val norm_hhf_prop = Logic.dest_equals (Thm.prop_of norm_hhf_eq);
--- a/src/Pure/goal_display.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/goal_display.ML Sun Apr 06 17:19:08 2014 +0200
@@ -23,13 +23,13 @@
structure Goal_Display: GOAL_DISPLAY =
struct
-val goals_limit_raw = Config.declare_option "goals_limit";
+val goals_limit_raw = Config.declare_option ("goals_limit", @{here});
val goals_limit = Config.int goals_limit_raw;
-val show_main_goal_raw = Config.declare_option "show_main_goal";
+val show_main_goal_raw = Config.declare_option ("show_main_goal", @{here});
val show_main_goal = Config.bool show_main_goal_raw;
-val show_consts_raw = Config.declare_option "show_consts";
+val show_consts_raw = Config.declare_option ("show_consts", @{here});
val show_consts = Config.bool show_consts_raw;
fun pretty_flexpair ctxt (t, u) = Pretty.block
--- a/src/Pure/pattern.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/pattern.ML Sun Apr 06 17:19:08 2014 +0200
@@ -42,7 +42,8 @@
val unify_trace_failure_default = Unsynchronized.ref false;
val unify_trace_failure_raw =
- Config.declare_global "unify_trace_failure" (fn _ => Config.Bool (! unify_trace_failure_default));
+ Config.declare_global ("unify_trace_failure", @{here})
+ (fn _ => Config.Bool (! unify_trace_failure_default));
val unify_trace_failure = Config.bool unify_trace_failure_raw;
fun string_of_term thy env binders t =
--- a/src/Pure/pure_thy.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/pure_thy.ML Sun Apr 06 17:19:08 2014 +0200
@@ -62,12 +62,12 @@
(Sign.map_naming (Name_Space.set_theory_name Context.PureN) #>
Old_Appl_Syntax.put false #>
Sign.add_types_global
- [(Binding.name "fun", 2, NoSyn),
- (Binding.name "prop", 0, NoSyn),
- (Binding.name "itself", 1, NoSyn),
- (Binding.name "dummy", 0, NoSyn)]
+ [(Binding.make ("fun", @{here}), 2, NoSyn),
+ (Binding.make ("prop", @{here}), 0, NoSyn),
+ (Binding.make ("itself", @{here}), 1, NoSyn),
+ (Binding.make ("dummy", @{here}), 0, NoSyn)]
#> Sign.add_nonterminals_global
- (map Binding.name
+ (map (fn name => Binding.make (name, @{here}))
(Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
"args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms",
"any", "prop'", "num_const", "float_const", "xnum_const", "num_position",
@@ -195,12 +195,12 @@
#> Sign.add_syntax ("HTML", false)
[("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
#> Sign.add_consts
- [(qualify (Binding.name "eq"), typ "'a => 'a => prop", Infix ("==", 2)),
- (qualify (Binding.name "imp"), typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
- (qualify (Binding.name "all"), typ "('a => prop) => prop", Binder ("!!", 0, 0)),
- (qualify (Binding.name "prop"), typ "prop => prop", NoSyn),
- (qualify (Binding.name "type"), typ "'a itself", NoSyn),
- (qualify (Binding.name "dummy_pattern"), typ "'a", Delimfix "'_")]
+ [(qualify (Binding.make ("eq", @{here})), typ "'a => 'a => prop", Infix ("==", 2)),
+ (qualify (Binding.make ("imp", @{here})), typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
+ (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", Binder ("!!", 0, 0)),
+ (qualify (Binding.make ("prop", @{here})), typ "prop => prop", NoSyn),
+ (qualify (Binding.make ("type", @{here})), typ "'a itself", NoSyn),
+ (qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", Delimfix "'_")]
#> Theory.add_deps_global "Pure.eq" ("Pure.eq", typ "'a => 'a => prop") []
#> Theory.add_deps_global "Pure.imp" ("Pure.imp", typ "prop => prop => prop") []
#> Theory.add_deps_global "Pure.all" ("Pure.all", typ "('a => prop) => prop") []
@@ -210,19 +210,22 @@
#> Sign.parse_translation Syntax_Trans.pure_parse_translation
#> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation
#> Sign.add_consts
- [(qualify (Binding.name "term"), typ "'a => prop", NoSyn),
- (qualify (Binding.name "sort_constraint"), typ "'a itself => prop", NoSyn),
- (qualify (Binding.name "conjunction"), typ "prop => prop => prop", NoSyn)]
+ [(qualify (Binding.make ("term", @{here})), typ "'a => prop", NoSyn),
+ (qualify (Binding.make ("sort_constraint", @{here})), typ "'a itself => prop", NoSyn),
+ (qualify (Binding.make ("conjunction", @{here})), typ "prop => prop => prop", NoSyn)]
#> Sign.local_path
#> (Global_Theory.add_defs false o map Thm.no_attributes)
- [(Binding.name "prop_def", prop "(CONST Pure.prop :: prop => prop) (A::prop) == A::prop"),
- (Binding.name "term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
- (Binding.name "sort_constraint_def",
+ [(Binding.make ("prop_def", @{here}),
+ prop "(CONST Pure.prop :: prop => prop) (A::prop) == A::prop"),
+ (Binding.make ("term_def", @{here}),
+ prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
+ (Binding.make ("sort_constraint_def", @{here}),
prop "(CONST Pure.sort_constraint :: 'a itself => prop) (CONST Pure.type :: 'a itself) ==\
\ (CONST Pure.term :: 'a itself => prop) (CONST Pure.type :: 'a itself)"),
- (Binding.name "conjunction_def", prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
- #> Global_Theory.add_thmss [((Binding.name "nothing", []), [])] #> snd
+ (Binding.make ("conjunction_def", @{here}),
+ prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
+ #> Global_Theory.add_thmss [((Binding.make ("nothing", @{here}), []), [])] #> snd
#> fold (fn (a, prop) =>
- snd o Thm.add_axiom_global (Binding.name a, prop)) Proofterm.equality_axms);
+ snd o Thm.add_axiom_global (Binding.make (a, @{here}), prop)) Proofterm.equality_axms);
end;
--- a/src/Pure/raw_simplifier.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/raw_simplifier.ML Sun Apr 06 17:19:08 2014 +0200
@@ -394,12 +394,13 @@
(* simp depth *)
-val simp_depth_limit_raw = Config.declare "simp_depth_limit" (K (Config.Int 100));
+val simp_depth_limit_raw = Config.declare ("simp_depth_limit", @{here}) (K (Config.Int 100));
val simp_depth_limit = Config.int simp_depth_limit_raw;
val simp_trace_depth_limit_default = Unsynchronized.ref 1;
-val simp_trace_depth_limit_raw = Config.declare "simp_trace_depth_limit"
- (fn _ => Config.Int (! simp_trace_depth_limit_default));
+val simp_trace_depth_limit_raw =
+ Config.declare ("simp_trace_depth_limit", @{here})
+ (fn _ => Config.Int (! simp_trace_depth_limit_default));
val simp_trace_depth_limit = Config.int simp_trace_depth_limit_raw;
fun inc_simp_depth ctxt =
@@ -418,11 +419,12 @@
exception SIMPLIFIER of string * thm list;
-val simp_debug_raw = Config.declare "simp_debug" (K (Config.Bool false));
+val simp_debug_raw = Config.declare ("simp_debug", @{here}) (K (Config.Bool false));
val simp_debug = Config.bool simp_debug_raw;
val simp_trace_default = Unsynchronized.ref false;
-val simp_trace_raw = Config.declare "simp_trace" (fn _ => Config.Bool (! simp_trace_default));
+val simp_trace_raw =
+ Config.declare ("simp_trace", @{here}) (fn _ => Config.Bool (! simp_trace_default));
val simp_trace = Config.bool simp_trace_raw;
fun cond_warning ctxt msg =
--- a/src/Pure/skip_proof.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/skip_proof.ML Sun Apr 06 17:19:08 2014 +0200
@@ -4,6 +4,9 @@
Skip proof via oracle invocation.
*)
+val quick_and_dirty_raw = Config.declare_option ("quick_and_dirty", @{here});
+val quick_and_dirty = Config.bool quick_and_dirty_raw;
+
signature SKIP_PROOF =
sig
val report: Proof.context -> unit
@@ -26,7 +29,8 @@
(* oracle setup *)
val (_, make_thm_cterm) =
- Context.>>> (Context.map_theory_result (Thm.add_oracle (Binding.name "skip_proof", I)));
+ Context.>>>
+ (Context.map_theory_result (Thm.add_oracle (Binding.make ("skip_proof", @{here}), I)));
fun make_thm thy prop = make_thm_cterm (Thm.cterm_of thy prop);
--- a/src/Pure/type_infer_context.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/type_infer_context.ML Sun Apr 06 17:19:08 2014 +0200
@@ -20,7 +20,8 @@
(* constraints *)
-val const_sorts = Config.bool (Config.declare "const_sorts" (K (Config.Bool true)));
+val const_sorts =
+ Config.bool (Config.declare ("const_sorts", @{here}) (K (Config.Bool true)));
fun const_type ctxt =
try ((not (Config.get ctxt const_sorts) ? Type.strip_sorts) o
--- a/src/Pure/unify.ML Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Pure/unify.ML Sun Apr 06 17:19:08 2014 +0200
@@ -34,19 +34,19 @@
(*Unification options*)
(*tracing starts above this depth, 0 for full*)
-val trace_bound_raw = Config.declare_global "unify_trace_bound" (K (Config.Int 50));
+val trace_bound_raw = Config.declare_global ("unify_trace_bound", @{here}) (K (Config.Int 50));
val trace_bound = Config.int trace_bound_raw;
(*unification quits above this depth*)
-val search_bound_raw = Config.declare_global "unify_search_bound" (K (Config.Int 60));
+val search_bound_raw = Config.declare_global ("unify_search_bound", @{here}) (K (Config.Int 60));
val search_bound = Config.int search_bound_raw;
(*print dpairs before calling SIMPL*)
-val trace_simp_raw = Config.declare_global "unify_trace_simp" (K (Config.Bool false));
+val trace_simp_raw = Config.declare_global ("unify_trace_simp", @{here}) (K (Config.Bool false));
val trace_simp = Config.bool trace_simp_raw;
(*announce potential incompleteness of type unification*)
-val trace_types_raw = Config.declare_global "unify_trace_types" (K (Config.Bool false));
+val trace_types_raw = Config.declare_global ("unify_trace_types", @{here}) (K (Config.Bool false));
val trace_types = Config.bool trace_types_raw;
--- a/src/Tools/jEdit/src/rich_text_area.scala Sun Apr 06 17:18:57 2014 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala Sun Apr 06 17:19:08 2014 +0200
@@ -167,7 +167,13 @@
override def mouseClicked(e: MouseEvent) {
robust_body(()) {
hyperlink_area.info match {
- case Some(Text.Info(_, link)) =>
+ case Some(Text.Info(range, link)) =>
+ try { text_area.moveCaretPosition(range.start) }
+ catch {
+ case _: ArrayIndexOutOfBoundsException =>
+ case _: IllegalArgumentException =>
+ }
+ text_area.requestFocus
link.follow(view)
case None =>
}