# HG changeset patch # User wenzelm # Date 1403890712 -7200 # Node ID 9188d901209d41c79b272fef9d888f17c6112033 # Parent e1afb42be5ad326b2a123af9edfed9c538034b8d# Parent e721124f1b1ebb3dd55fd4e1b7cd0bcdf827d39f merged diff -r e1afb42be5ad -r 9188d901209d Admin/MacOS/Info.plist-part2 --- 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 @@ -Disabelle.home=$APP_ROOT/Contents/Resources/{ISABELLE_NAME} +-Disabelle.app=true JVMArguments diff -r e1afb42be5ad -r 9188d901209d NEWS --- 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. diff -r e1afb42be5ad -r 9188d901209d etc/isar-keywords-ZF.el --- 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" diff -r e1afb42be5ad -r 9188d901209d etc/isar-keywords.el --- 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" diff -r e1afb42be5ad -r 9188d901209d lib/Tools/emacs --- 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 diff -r e1afb42be5ad -r 9188d901209d lib/Tools/findlogics --- 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") diff -r e1afb42be5ad -r 9188d901209d lib/Tools/unsymbolize --- 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. \)." - 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" diff -r e1afb42be5ad -r 9188d901209d lib/scripts/getsettings --- 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 diff -r e1afb42be5ad -r 9188d901209d lib/scripts/unsymbolize --- 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 = ; $/ = "\n"; # slurp whole file - close FILE || die $!; - - $_ = $text; - - # Pure - s/\\?\\/!!/g; - s/\\?\\/::/g; - s/\\?\\/==>/g; - s/\\?\\\\?\\/==>/g; - s/\\?\\/=>/g; - s/\\?\\/==/g; - s/\\?\\/.../g; - s/\\?\\ ?/[| /g; - s/\\?\\ ?/ |]/g; - s/\\?\\ ?/(| /g; - s/\\?\\ ?/ |)/g; - # HOL - s/\\?\\/<->/g; - s/\\?\\/-->/g; - s/\\?\\\\?\\/-->/g; - s/\\?\\/->/g; - s/\\?\\/~/g; - s/\\?\\/~:/g; - s/\\?\\/~=/g; - s/\\?\\ ?/SOME /g; - # outer syntax - s/\\?\\/==/g; - s/\\?\\/=>/g; - s/\\?\\/<=/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"; } -} diff -r e1afb42be5ad -r 9188d901209d src/Doc/Isar_Ref/Misc.thy --- 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 \"} \\ @{command_def "unused_thms"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \"} \\ - @{command_def "print_binds"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def "print_term_bindings"}@{text "\<^sup>*"} & : & @{text "context \"} \\ \end{matharray} @{rail \ @@ -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 diff -r e1afb42be5ad -r 9188d901209d src/Doc/JEdit/JEdit.thy --- 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}. *} diff -r e1afb42be5ad -r 9188d901209d src/Doc/System/Misc.thy --- 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 ""} - 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 {* diff -r e1afb42be5ad -r 9188d901209d src/HOL/Library/README.html --- 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 @@
-
Files - -
Avoid unnecessary scattering of theories over several files. Use -new-style theories only, as old ones tend to clutter the file space -with separate .thy and .ML files. -
Examples
Theories should be as ``generic'' as is sensible. Unused (or @@ -54,12 +48,6 @@ separate word constituents by underscores, as in foo_bar or Foo_Bar (this looks best in LaTeX output). -

- -Note that syntax is global; qualified names lose syntax on -output. Do not use ``exotic'' symbols for syntax (such as -\<oplus>), but leave these for user applications. -

Global context declarations
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. -
Mathematical symbols - -
Non-ASCII symbols should be used as appropriate, with some -care. In particular, avoid unreadable arrows: ==> should -be preferred over \<Longrightarrow>. Use isabelle -unsymbolize to clean up the sources. - -

- -The following ASCII symbols of HOL should be generally avoided: -@, !, ?, ?!, %, better -use SOME, ALL (or \<forall>), -EX (or \<exists>), EX! (or -\<exists>!), \<lambda>, respectively. -Note that bracket notation [| |] looks bad in LaTeX -output. - -

- -Some additional mathematical symbols are quite suitable for both -readable sources and the output document: -\<Inter>, -\<Union>, -\<and>, -\<in>, -\<inter>, -\<le>, -\<not>, -\<noteq>, -\<notin>, -\<or>, -\<subset>, -\<subseteq>, -\<times>, -\<union>. -

Spacing
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 after each punctuation character (",", ".", etc.), but none -before it; do not extra spaces inside of parentheses, unless the -delimiters are composed of multiple symbols (as in -[| |]); 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.
diff -r e1afb42be5ad -r 9188d901209d src/Pure/Isar/isar_syn.ML --- 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" diff -r e1afb42be5ad -r 9188d901209d src/Pure/Isar/proof_context.ML --- 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))) @ diff -r e1afb42be5ad -r 9188d901209d src/Pure/Pure.thy --- 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 diff -r e1afb42be5ad -r 9188d901209d src/Pure/System/isabelle_system.scala --- 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 diff -r e1afb42be5ad -r 9188d901209d src/Pure/Tools/print_operation.ML --- 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"