--- a/Admin/MacOS/Info.plist-part2 Fri Jun 27 19:21:58 2014 +0200
+++ b/Admin/MacOS/Info.plist-part2 Fri Jun 27 19:38:32 2014 +0200
@@ -1,4 +1,5 @@
<string>-Disabelle.home=$APP_ROOT/Contents/Resources/{ISABELLE_NAME}</string>
+<string>-Disabelle.app=true</string>
</array>
<key>JVMArguments</key>
<array>
--- a/NEWS Fri Jun 27 19:21:58 2014 +0200
+++ b/NEWS Fri Jun 27 19:38:32 2014 +0200
@@ -205,6 +205,9 @@
(only makes sense in practice, if outer syntax is delimited
differently).
+* Command 'print_term_bindings' supersedes 'print_binds' for clarity,
+but the latter is retained some time as Proof General legacy.
+
*** HOL ***
@@ -855,6 +858,10 @@
incompatibility for old tools that do not use the $ISABELLE_PROCESS
settings variable yet.
+* Removed obsolete "isabelle unsymbolize". Note that the usual format
+for email communication is the Unicode rendering of Isabelle symbols,
+as produced by Isabelle/jEdit, for example.
+
* Retired the now unused Isabelle tool "wwwfind". Similar
functionality may be integrated into PIDE/jEdit at a later point.
--- a/etc/isar-keywords-ZF.el Fri Jun 27 19:21:58 2014 +0200
+++ b/etc/isar-keywords-ZF.el Fri Jun 27 19:38:32 2014 +0200
@@ -147,6 +147,7 @@
"print_statement"
"print_syntax"
"print_tcset"
+ "print_term_bindings"
"print_theorems"
"print_theory"
"print_trans_rules"
@@ -316,6 +317,7 @@
"print_statement"
"print_syntax"
"print_tcset"
+ "print_term_bindings"
"print_theorems"
"print_theory"
"print_trans_rules"
--- a/etc/isar-keywords.el Fri Jun 27 19:21:58 2014 +0200
+++ b/etc/isar-keywords.el Fri Jun 27 19:38:32 2014 +0200
@@ -213,6 +213,7 @@
"print_state"
"print_statement"
"print_syntax"
+ "print_term_bindings"
"print_theorems"
"print_theory"
"print_trans_rules"
@@ -445,6 +446,7 @@
"print_state"
"print_statement"
"print_syntax"
+ "print_term_bindings"
"print_theorems"
"print_theory"
"print_trans_rules"
--- a/lib/Tools/emacs Fri Jun 27 19:21:58 2014 +0200
+++ b/lib/Tools/emacs Fri Jun 27 19:38:32 2014 +0200
@@ -2,7 +2,7 @@
#
# Author: Makarius
#
-# DESCRIPTION: Proof General / Emacs interface wrapper
+# DESCRIPTION: Proof General / Emacs interface wrapper -- Proof General legacy
## diagnostics
--- a/lib/Tools/findlogics Fri Jun 27 19:21:58 2014 +0200
+++ b/lib/Tools/findlogics Fri Jun 27 19:38:32 2014 +0200
@@ -2,7 +2,7 @@
#
# Author: Markus Wenzel, TU Muenchen
#
-# DESCRIPTION: collect heap names from ISABELLE_PATH
+# DESCRIPTION: collect heap names from ISABELLE_PATH -- Proof General legacy
PRG=$(basename "$0")
--- a/lib/Tools/unsymbolize Fri Jun 27 19:21:58 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# DESCRIPTION: remove unreadable symbol names from sources
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG [FILES|DIRS...]"
- echo
- echo " Recursively find .thy/.ML files and remove symbols that are unreadably"
- echo " in plain text (e.g. \<Longrightarrow>)."
- echo
- echo " Note: this is an ad-hoc script; there is no systematic way to replace"
- echo " symbols independently of the inner syntax of a theory!"
- echo
- echo " Old versions of files are preserved by appending \"~~\"."
- echo
- exit 1
-}
-
-
-## process command line
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
-
-SPECS="$@"; shift "$#"
-
-
-## main
-
-find $SPECS \( -name \*.ML -o -name \*.thy \) -print0 | \
- xargs -0 "$ISABELLE_HOME/lib/scripts/unsymbolize"
--- a/lib/scripts/getsettings Fri Jun 27 19:21:58 2014 +0200
+++ b/lib/scripts/getsettings Fri Jun 27 19:38:32 2014 +0200
@@ -16,6 +16,11 @@
function tar() { /usr/bin/gnutar "$@"; }
fi
+#sane environment defaults (notably on Mac OS X)
+if [ "$ISABELLE_APP" = true -a -x /usr/libexec/path_helper ]; then
+ eval $(/usr/libexec/path_helper -s)
+fi
+
#Cygwin vs. POSIX
if [ "$OSTYPE" = cygwin ]
then
--- a/lib/scripts/unsymbolize Fri Jun 27 19:21:58 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-#!/usr/bin/env perl
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# unsymbolize - remove unreadable symbol names from sources
-
-use warnings;
-use strict;
-
-sub unsymbolize {
- my ($file) = @_;
-
- open (FILE, $file) || die $!;
- undef $/; my $text = <FILE>; $/ = "\n"; # slurp whole file
- close FILE || die $!;
-
- $_ = $text;
-
- # Pure
- s/\\?\\<And>/!!/g;
- s/\\?\\<Colon>/::/g;
- s/\\?\\<Longrightarrow>/==>/g;
- s/\\?\\<Midarrow>\\?\\<Rightarrow>/==>/g;
- s/\\?\\<Rightarrow>/=>/g;
- s/\\?\\<equiv>/==/g;
- s/\\?\\<dots>/.../g;
- s/\\?\\<lbrakk> ?/[| /g;
- s/\\?\\ ?<rbrakk>/ |]/g;
- s/\\?\\<lparr> ?/(| /g;
- s/\\?\\ ?<rparr>/ |)/g;
- # HOL
- s/\\?\\<longleftrightarrow>/<->/g;
- s/\\?\\<longrightarrow>/-->/g;
- s/\\?\\<midarrow>\\?\\<rightarrow>/-->/g;
- s/\\?\\<rightarrow>/->/g;
- s/\\?\\<not>/~/g;
- s/\\?\\<notin>/~:/g;
- s/\\?\\<noteq>/~=/g;
- s/\\?\\<some> ?/SOME /g;
- # outer syntax
- s/\\?\\<rightleftharpoons>/==/g;
- s/\\?\\<rightharpoonup>/=>/g;
- s/\\?\\<leftharpoondown>/<=/g;
-
- my $result = $_;
-
- if ($text ne $result) {
- print STDERR "changing $file\n";
- if (! -f "$file~~") {
- rename $file, "$file~~" || die $!;
- }
- open (FILE, "> $file") || die $!;
- print FILE $result;
- close FILE || die $!;
- }
-}
-
-
-## main
-
-foreach my $file (@ARGV) {
- eval { &unsymbolize($file); };
- if ($@) { print STDERR "*** unsymbolize $file: ", $@, "\n"; }
-}
--- a/src/Doc/Isar_Ref/Misc.thy Fri Jun 27 19:21:58 2014 +0200
+++ b/src/Doc/Isar_Ref/Misc.thy Fri Jun 27 19:38:32 2014 +0200
@@ -17,7 +17,7 @@
@{command_def "thm_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "unused_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{command_def "print_binds"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "print_term_bindings"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
\end{matharray}
@{rail \<open>
@@ -63,8 +63,8 @@
current context, both named and unnamed ones; the ``@{text "!"}''
option indicates extra verbosity.
- \item @{command "print_binds"} prints all term abbreviations
- present in the context.
+ \item @{command "print_term_bindings"} prints all term bindings that
+ are present in the context.
\item @{command "find_theorems"}~@{text criteria} retrieves facts
from the theory or proof context matching all of given search
--- a/src/Doc/JEdit/JEdit.thy Fri Jun 27 19:21:58 2014 +0200
+++ b/src/Doc/JEdit/JEdit.thy Fri Jun 27 19:38:32 2014 +0200
@@ -960,8 +960,8 @@
The \emph{Query} panel in \emph{Print Context} mode prints information from
the theory or proof context, or proof state. See also the Isar commands
@{command_ref print_context}, @{command_ref print_cases}, @{command_ref
- print_binds}, @{command_ref print_theorems}, @{command_ref print_state} in
- \cite{isabelle-isar-ref}.
+ print_term_bindings}, @{command_ref print_theorems},
+ @{command_ref print_state} in \cite{isabelle-isar-ref}.
*}
--- a/src/Doc/System/Misc.thy Fri Jun 27 19:21:58 2014 +0200
+++ b/src/Doc/System/Misc.thy Fri Jun 27 19:38:32 2014 +0200
@@ -318,25 +318,6 @@
*}
-section {* Getting logic images *}
-
-text {* The @{tool_def findlogics} tool traverses all directories
- specified in @{setting ISABELLE_PATH}, looking for Isabelle logic
- images. Its usage is:
-\begin{ttbox}
-Usage: isabelle findlogics
-
- Collect heap file names from ISABELLE_PATH.
-\end{ttbox}
-
- The base names of all files found on the path are printed --- sorted
- and with duplicates removed. Also note that lookup in @{setting
- ISABELLE_PATH} includes the current values of @{setting ML_SYSTEM}
- and @{setting ML_PLATFORM}. Thus switching to another ML compiler
- may change the set of logic images available.
-*}
-
-
section {* Inspecting the settings environment \label{sec:tool-getenv} *}
text {* The Isabelle settings environment --- as provided by the
@@ -472,26 +453,6 @@
"();"} in ML will return to the Isar toplevel. *}
-section {* Remove awkward symbol names from theory sources *}
-
-text {*
- The @{tool_def unsymbolize} tool tunes Isabelle theory sources to
- improve readability for plain ASCII output (e.g.\ in email
- communication). Most notably, @{tool unsymbolize} replaces awkward
- arrow symbols such as @{verbatim "\\"}@{verbatim "<Longrightarrow>"}
- by @{verbatim "==>"}.
-\begin{ttbox}
-Usage: isabelle unsymbolize [FILES|DIRS...]
-
- Recursively find .thy/.ML files, removing unreadable symbol names.
- Note: this is an ad-hoc script; there is no systematic way to replace
- symbols independently of the inner syntax of a theory!
-
- Renames old versions of FILES by appending "~~".
-\end{ttbox}
-*}
-
-
section {* Output the version identifier of the Isabelle distribution *}
text {*
--- a/src/HOL/Library/README.html Fri Jun 27 19:21:58 2014 +0200
+++ b/src/HOL/Library/README.html Fri Jun 27 19:38:32 2014 +0200
@@ -23,12 +23,6 @@
<dl>
-<dt><strong>Files</strong>
-
-<dd>Avoid unnecessary scattering of theories over several files. Use
-new-style theories only, as old ones tend to clutter the file space
-with separate <tt>.thy</tt> and <tt>.ML</tt> files.
-
<dt><strong>Examples</strong>
<dd>Theories should be as ``generic'' as is sensible. Unused (or
@@ -54,12 +48,6 @@
separate word constituents by underscores, as in <tt>foo_bar</tt> or
<tt>Foo_Bar</tt> (this looks best in LaTeX output).
-<p>
-
-Note that syntax is <em>global</em>; qualified names lose syntax on
-output. Do not use ``exotic'' symbols for syntax (such as
-<tt>\<oplus></tt>), but leave these for user applications.
-
<dt><strong>Global context declarations</strong>
<dd>Only items introduced in the present theory should be declared
@@ -67,42 +55,6 @@
rules from parent theories may result in strange behavior later,
depending on the user's arrangement of import lists.
-<dt><strong>Mathematical symbols</strong>
-
-<dd>Non-ASCII symbols should be used as appropriate, with some
-care. In particular, avoid unreadable arrows: <tt>==></tt> should
-be preferred over <tt>\<Longrightarrow></tt>. Use <tt>isabelle
-unsymbolize</tt> to clean up the sources.
-
-<p>
-
-The following ASCII symbols of HOL should be generally avoided:
-<tt>@</tt>, <tt>!</tt>, <tt>?</tt>, <tt>?!</tt>, <tt>%</tt>, better
-use <tt>SOME</tt>, <tt>ALL</tt> (or <tt>\<forall></tt>),
-<tt>EX</tt> (or <tt>\<exists></tt>), <tt>EX!</tt> (or
-<tt>\<exists>!</tt>), <tt>\<lambda></tt>, respectively.
-Note that bracket notation <tt>[| |]</tt> looks bad in LaTeX
-output.
-
-<p>
-
-Some additional mathematical symbols are quite suitable for both
-readable sources and the output document:
-<tt>\<Inter></tt>,
-<tt>\<Union></tt>,
-<tt>\<and></tt>,
-<tt>\<in></tt>,
-<tt>\<inter></tt>,
-<tt>\<le></tt>,
-<tt>\<not></tt>,
-<tt>\<noteq></tt>,
-<tt>\<notin></tt>,
-<tt>\<or></tt>,
-<tt>\<subset></tt>,
-<tt>\<subseteq></tt>,
-<tt>\<times></tt>,
-<tt>\<union></tt>.
-
<dt><strong>Spacing</strong>
<dd>Isabelle is able to produce a high-quality LaTeX document from the
@@ -111,10 +63,8 @@
text. Incidentally, output looks very good if common type-setting
conventions are observed: put a single space <em>after</em> each
punctuation character ("<tt>,</tt>", "<tt>.</tt>", etc.), but none
-before it; do not extra spaces inside of parentheses, unless the
-delimiters are composed of multiple symbols (as in
-<tt>[| |]</tt>); do not attempt to simulate table markup with
-spaces, avoid ``hanging'' indentations.
+before it; do not extra spaces inside of parentheses; do not attempt
+to simulate table markup with spaces, avoid ``hanging'' indentations.
</dl>
--- a/src/Pure/Isar/isar_syn.ML Fri Jun 27 19:21:58 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML Fri Jun 27 19:38:32 2014 +0200
@@ -897,9 +897,18 @@
(Parse_Spec.xthms1 >> Isar_Cmd.thm_deps);
val _ =
- Outer_Syntax.improper_command @{command_spec "print_binds"} "print term bindings of proof context"
+ 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_binds o Toplevel.context_of)));
+ 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
+ Toplevel.keep
+ (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
val _ =
Outer_Syntax.improper_command @{command_spec "print_facts"} "print facts of proof context"
--- a/src/Pure/Isar/proof_context.ML Fri Jun 27 19:21:58 2014 +0200
+++ b/src/Pure/Isar/proof_context.ML Fri Jun 27 19:38:32 2014 +0200
@@ -161,7 +161,7 @@
val generic_revert_abbrev: string -> string -> Context.generic -> Context.generic
val print_syntax: Proof.context -> unit
val print_abbrevs: Proof.context -> unit
- val pretty_binds: Proof.context -> Pretty.T list
+ val pretty_term_bindings: Proof.context -> Pretty.T list
val pretty_local_facts: Proof.context -> bool -> Pretty.T list
val print_local_facts: Proof.context -> bool -> unit
val pretty_cases: Proof.context -> Pretty.T list
@@ -1257,7 +1257,7 @@
(* term bindings *)
-fun pretty_binds ctxt =
+fun pretty_term_bindings ctxt =
let
val binds = Variable.binds_of ctxt;
fun prt_bind (xi, (T, t)) = pretty_term_abbrev ctxt (Logic.mk_equals (Var (xi, T), t));
@@ -1408,7 +1408,7 @@
verb single (K pretty_thy) @
pretty_ctxt ctxt @
verb (pretty_abbrevs false) (K ctxt) @
- verb pretty_binds (K ctxt) @
+ verb pretty_term_bindings (K ctxt) @
verb (pretty_local_facts ctxt) (K true) @
verb pretty_cases (K ctxt) @
verb single (fn () => Pretty.big_list "type constraints:" (map prt_defT (Vartab.dest types))) @
--- a/src/Pure/Pure.thy Fri Jun 27 19:21:58 2014 +0200
+++ b/src/Pure/Pure.thy Fri Jun 27 19:38:32 2014 +0200
@@ -85,10 +85,9 @@
"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_facts"
- "print_cases" "print_statement" "thm" "prf" "full_prf" "prop"
- "term" "typ" "print_codesetup" "unused_thms"
- :: diag
+ "locale_deps" "class_deps" "thm_deps" "print_binds" "print_term_bindings"
+ "print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf"
+ "prop" "term" "typ" "print_codesetup" "unused_thms" :: diag
and "cd" :: control
and "pwd" :: diag
and "use_thy" "remove_thy" "kill_thy" :: control
--- a/src/Pure/System/isabelle_system.scala Fri Jun 27 19:21:58 2014 +0200
+++ b/src/Pure/System/isabelle_system.scala Fri Jun 27 19:38:32 2014 +0200
@@ -75,12 +75,22 @@
}
set_cygwin_root()
- val env0 = sys.env + ("ISABELLE_JDK_HOME" -> posix_path(jdk_home()))
+
+ val env =
+ {
+ val user_home = System.getProperty("user.home", "")
+ val isabelle_app = System.getProperty("isabelle.app", "")
- val user_home = System.getProperty("user.home", "")
- val env =
- if (user_home == "" || env0.isDefinedAt("HOME")) env0
- else env0 + ("HOME" -> user_home)
+ val env0 = sys.env + ("ISABELLE_JDK_HOME" -> posix_path(jdk_home()))
+ val env1 =
+ if (user_home == "" || env0.isDefinedAt("HOME")) env0
+ else env0 + ("HOME" -> user_home)
+ val env2 =
+ if (isabelle_app == "") env1
+ else env1 + ("ISABELLE_APP" -> "true")
+
+ env2
+ }
val system_home =
if (isabelle_home != null && isabelle_home != "") isabelle_home
--- a/src/Pure/Tools/print_operation.ML Fri Jun 27 19:21:58 2014 +0200
+++ b/src/Pure/Tools/print_operation.ML Fri Jun 27 19:38:32 2014 +0200
@@ -70,7 +70,7 @@
val _ =
register "terms" "term bindings of proof context"
- (Pretty.string_of o Pretty.chunks o Proof_Context.pretty_binds o Toplevel.context_of);
+ (Pretty.string_of o Pretty.chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of);
val _ =
register "theorems" "theorems of local theory or proof context"