merged
authorwenzelm
Mon, 06 Jan 2014 23:00:11 +0100
changeset 54940 a20b105bb5d1
parent 54934 4587de627cd8 (current diff)
parent 54939 b411e99d1581 (diff)
child 54941 6d99745afe34
merged
etc/proofgeneral-settings.el
etc/user-settings.sample
--- a/etc/proofgeneral-settings.el	Mon Jan 06 19:55:01 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-;;; Options for Proof General
-;;;
-;;; Examples for sensible settings:
-
-;; keep sources clean
-(custom-set-variables '(indent-tabs-mode nil))
-
-;; retain vital AltGr behaviour, e.g. on non-US Mac OS X
-;(custom-set-variables '(ns-alternate-modifier 'none))
-
-;; longer timeout for saving persistent session
-;(custom-set-variables '(proof-shell-quit-timeout 60))
-
--- a/etc/settings	Mon Jan 06 19:55:01 2014 +0100
+++ b/etc/settings	Mon Jan 06 23:00:11 2014 +0100
@@ -1,11 +1,12 @@
 # -*- shell-script -*- :mode=shellscript:
 #
-# Isabelle settings -- distribution defaults.
+# Isabelle system settings.
 #
 # Important notes:
 #   * See the "system" manual for explanations on Isabelle settings
+#   * User settings go into $ISABELLE_HOME_USER/etc/settings
 #   * DO NOT EDIT the repository copy of this file!
-#   * DO NOT COPY this file into your ~/.isabelle directory!
+#   * DO NOT COPY this file into the $ISABELLE_HOME_USER directory!
 
 ###
 ### Isabelle/Scala
--- a/etc/user-settings.sample	Mon Jan 06 19:55:01 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-#
-# Isabelle user settings sample -- for use in $ISABELLE_HOME_USER/etc/settings
-
-ISABELLE_BUILD_OPTIONS="browser_info document=pdf"
-ISABELLE_LOGIC=HOL
--- a/src/Doc/System/Basics.thy	Mon Jan 06 19:55:01 2014 +0100
+++ b/src/Doc/System/Basics.thy	Mon Jan 06 23:00:11 2014 +0100
@@ -101,14 +101,10 @@
   before --- usually to something like @{verbatim
   "$USER_HOME/.isabelle/IsabelleXXXX"}.
   
-  Thus individual users may override the site-wide defaults.  See also
-  file @{file "$ISABELLE_HOME/etc/user-settings.sample"} in the
-  distribution.  Typically, a user settings file would contain only a
-  few lines, just the assigments that are really changed.  One should
-  definitely \emph{not} start with a full copy the basic @{file
-  "$ISABELLE_HOME/etc/settings"}. This could cause very annoying
-  maintainance problems later, when the Isabelle installation is
-  updated or changed otherwise.
+  Thus individual users may override the site-wide defaults.
+  Typically, a user settings file contains only a few lines, with some
+  assignments that are actually changed.  Never copy the central
+  @{file "$ISABELLE_HOME/etc/settings"} file!
   
   \end{enumerate}
 
--- a/src/Doc/System/Presentation.thy	Mon Jan 06 19:55:01 2014 +0100
+++ b/src/Doc/System/Presentation.thy	Mon Jan 06 23:00:11 2014 +0100
@@ -310,7 +310,7 @@
   inspect {\LaTeX} runs in further detail, e.g.\ like this:
 
 \begin{ttbox}
-  cd ~/.isabelle/IsabelleXXXX/browser_info/Unsorted/Test/document
+  cd "$(isabelle getenv -b ISABELLE_BROWSER_INFO)/Unsorted/Test/document"
   isabelle latex -o pdf
 \end{ttbox}
 *}
--- a/src/Doc/Tutorial/Documents/Documents.thy	Mon Jan 06 19:55:01 2014 +0100
+++ b/src/Doc/Tutorial/Documents/Documents.thy	Mon Jan 06 23:00:11 2014 +0100
@@ -343,7 +343,8 @@
   session is derived from a single parent, usually an object-logic
   image like \texttt{HOL}.  This results in an overall tree structure,
   which is reflected by the output location in the file system
-  (usually rooted at \verb,~/.isabelle/IsabelleXXXX/browser_info,).
+  (the root directory is determined by the Isabelle settings variable
+  \verb,ISABELLE_BROWSER_INFO,).
 
   \medskip The easiest way to manage Isabelle sessions is via
   \texttt{isabelle mkroot} (to generate an initial session source
--- a/src/Pure/Tools/build.scala	Mon Jan 06 19:55:01 2014 +0100
+++ b/src/Pure/Tools/build.scala	Mon Jan 06 23:00:11 2014 +0100
@@ -117,7 +117,8 @@
         (Graph.string[Session_Info] /: infos) {
           case (graph, (name, info)) =>
             if (graph.defined(name))
-              error("Duplicate session " + quote(name) + Position.here(info.pos))
+              error("Duplicate session " + quote(name) + Position.here(info.pos) +
+                Position.here(graph.get_node(name).pos))
             else graph.new_node(name, info)
         }
       val graph2 =