merged
authorwenzelm
Tue Aug 14 16:18:15 2012 +0200 (2012-08-14)
changeset 48806559c1d80e129
parent 48803 ffa31bf5c662
parent 48805 c3ea910b3581
child 48807 fde8c3d84ff5
child 48809 2db8aa3459d4
merged
     1.1 --- a/Admin/Release/makedist	Tue Aug 14 16:09:45 2012 +0200
     1.2 +++ b/Admin/Release/makedist	Tue Aug 14 16:18:15 2012 +0200
     1.3 @@ -23,7 +23,6 @@
     1.4  Usage: $PRG [OPTIONS] [VERSION]
     1.5  
     1.6    Options are:
     1.7 -    -D                 retain doc-src component
     1.8      -j JEDIT_BUILD     build Isabelle/jEdit via given jedit_build component
     1.9      -r RELEASE         proper release with name"
    1.10  
    1.11 @@ -47,16 +46,12 @@
    1.12  
    1.13  # options
    1.14  
    1.15 -RETAIN_DOC_SRC=""
    1.16  RELEASE=""
    1.17  ISABELLE_JEDIT_BUILD_HOME=""
    1.18  
    1.19 -while getopts "Dj:r:" OPT
    1.20 +while getopts "j:r:" OPT
    1.21  do
    1.22    case "$OPT" in
    1.23 -    D)
    1.24 -      RETAIN_DOC_SRC=true
    1.25 -      ;;
    1.26      j)
    1.27        ISABELLE_JEDIT_BUILD_HOME="$OPTARG"
    1.28        ;;
    1.29 @@ -152,9 +147,7 @@
    1.30  
    1.31  perl -pi -e 's/^(ISABELLE_SCALA_BUILD_OPTIONS=")/$1-optimise /,' etc/settings
    1.32  
    1.33 -if [ -n "$RETAIN_DOC_SRC" ]; then
    1.34 -  cp -a doc-src doc-src.orig
    1.35 -fi
    1.36 +cp -a doc-src doc-src.orig
    1.37  
    1.38  ./Admin/build all || fail "Failed to build distribution"
    1.39  
    1.40 @@ -174,9 +167,7 @@
    1.41  rm doc/adaptation.dvi doc/adaptation.pdf doc/architecture.dvi doc/architecture.pdf
    1.42  rm -rf doc-src
    1.43  
    1.44 -if [ -n "$RETAIN_DOC_SRC" ]; then
    1.45 -  mv doc-src.orig doc-src
    1.46 -fi
    1.47 +mv doc-src.orig doc-src
    1.48  
    1.49  mkdir -p contrib
    1.50  cat >contrib/README <<EOF
     2.1 --- a/Admin/isatest/isatest-makedist	Tue Aug 14 16:09:45 2012 +0200
     2.2 +++ b/Admin/isatest/isatest-makedist	Tue Aug 14 16:18:15 2012 +0200
     2.3 @@ -60,7 +60,7 @@
     2.4  
     2.5  echo "### building distribution"  >> $DISTLOG 2>&1
     2.6  mkdir -p $DISTPREFIX
     2.7 -$MAKEDIST -D -j "/home/isabelle/contrib_devel/jedit_build-20120414" >> $DISTLOG 2>&1
     2.8 +$MAKEDIST -j "/home/isabelle/contrib_devel/jedit_build-20120414" >> $DISTLOG 2>&1
     2.9  
    2.10  if [ $? -ne 0 ]
    2.11  then
     3.1 --- a/NEWS	Tue Aug 14 16:09:45 2012 +0200
     3.2 +++ b/NEWS	Tue Aug 14 16:18:15 2012 +0200
     3.3 @@ -29,6 +29,12 @@
     3.4  operators like COMP, INCR_COMP, COMP_INCR, which need to be applied
     3.5  with some care where this is really required.
     3.6  
     3.7 +* Command 'typ' supports an additional variant with explicit sort
     3.8 +constraint, to infer and check the most general type conforming to a
     3.9 +given given sort.  Example (in HOL):
    3.10 +
    3.11 +  typ "_ * _ * bool * unit" :: finite
    3.12 +
    3.13  
    3.14  *** HOL ***
    3.15  
     4.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Tue Aug 14 16:09:45 2012 +0200
     4.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Tue Aug 14 16:18:15 2012 +0200
     4.3 @@ -47,7 +47,7 @@
     4.4    internal logical entities in a human-readable fashion.
     4.5  
     4.6    @{rail "
     4.7 -    @@{command typ} @{syntax modes}? @{syntax type}
     4.8 +    @@{command typ} @{syntax modes}? @{syntax type} ('::' @{syntax sort})?
     4.9      ;
    4.10      @@{command term} @{syntax modes}? @{syntax term}
    4.11      ;
    4.12 @@ -65,8 +65,15 @@
    4.13  
    4.14    \begin{description}
    4.15  
    4.16 -  \item @{command "typ"}~@{text \<tau>} reads and prints types of the
    4.17 -  meta-logic according to the current theory or proof context.
    4.18 +  \item @{command "typ"}~@{text \<tau>} reads and prints a type expression
    4.19 +  according to the current context.
    4.20 +
    4.21 +  \item @{command "typ"}~@{text "\<tau> :: s"} uses type-inference to
    4.22 +  determine the most general way to make @{text "\<tau>"} conform to sort
    4.23 +  @{text "s"}.  For concrete @{text "\<tau>"} this checks if the type
    4.24 +  belongs to that sort.  Dummy type parameters ``@{text "_"}''
    4.25 +  (underscore) are assigned to fresh type variables with most general
    4.26 +  sorts, according the the principles of type-inference.
    4.27  
    4.28    \item @{command "term"}~@{text t} and @{command "prop"}~@{text \<phi>}
    4.29    read, type-check and print terms or propositions according to the
     5.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Tue Aug 14 16:09:45 2012 +0200
     5.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Tue Aug 14 16:18:15 2012 +0200
     5.3 @@ -75,6 +75,11 @@
     5.4  \rail@nont{\hyperlink{syntax.modes}{\mbox{\isa{modes}}}}[]
     5.5  \rail@endbar
     5.6  \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
     5.7 +\rail@bar
     5.8 +\rail@nextbar{1}
     5.9 +\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
    5.10 +\rail@nont{\hyperlink{syntax.sort}{\mbox{\isa{sort}}}}[]
    5.11 +\rail@endbar
    5.12  \rail@end
    5.13  \rail@begin{2}{}
    5.14  \rail@term{\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}}[]
    5.15 @@ -139,8 +144,15 @@
    5.16  
    5.17    \begin{description}
    5.18  
    5.19 -  \item \hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}~\isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} reads and prints types of the
    5.20 -  meta-logic according to the current theory or proof context.
    5.21 +  \item \hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}~\isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} reads and prints a type expression
    5.22 +  according to the current context.
    5.23 +
    5.24 +  \item \hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ s{\isaliteral{22}{\isachardoublequote}}} uses type-inference to
    5.25 +  determine the most general way to make \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} conform to sort
    5.26 +  \isa{{\isaliteral{22}{\isachardoublequote}}s{\isaliteral{22}{\isachardoublequote}}}.  For concrete \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} this checks if the type
    5.27 +  belongs to that sort.  Dummy type parameters ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}}''
    5.28 +  (underscore) are assigned to fresh type variables with most general
    5.29 +  sorts, according the the principles of type-inference.
    5.30  
    5.31    \item \hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}~\isa{t} and \hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}~\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}}
    5.32    read, type-check and print terms or propositions according to the
     6.1 --- a/doc-src/System/Thy/Interfaces.thy	Tue Aug 14 16:09:45 2012 +0200
     6.2 +++ b/doc-src/System/Thy/Interfaces.thy	Tue Aug 14 16:18:15 2012 +0200
     6.3 @@ -15,6 +15,7 @@
     6.4    Options are:
     6.5      -J OPTION    add JVM runtime option (default JEDIT_JAVA_OPTIONS)
     6.6      -b           build only
     6.7 +    -d DIR       include session directory
     6.8      -f           fresh build
     6.9      -j OPTION    add jEdit runtime option (default JEDIT_OPTIONS)
    6.10      -l NAME      logic image name (default ISABELLE_LOGIC)
    6.11 @@ -24,8 +25,12 @@
    6.12  (default Scratch.thy).
    6.13  \end{ttbox}
    6.14  
    6.15 -  The @{verbatim "-l"} option specifies the logic image.  The
    6.16 -  @{verbatim "-m"} option specifies additional print modes.
    6.17 +  The @{verbatim "-l"} option specifies the session name of the logic
    6.18 +  image to be used for proof processing.  Additional session root
    6.19 +  directories may be included via option @{verbatim "-d"} to augment
    6.20 +  that name space (see also \secref{sec:tool-build}).
    6.21 +
    6.22 +  The @{verbatim "-m"} option specifies additional print modes.
    6.23  
    6.24    The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass
    6.25    additional low-level options to the JVM or jEdit, respectively.  The
     7.1 --- a/doc-src/System/Thy/Sessions.thy	Tue Aug 14 16:09:45 2012 +0200
     7.2 +++ b/doc-src/System/Thy/Sessions.thy	Tue Aug 14 16:18:15 2012 +0200
     7.3 @@ -356,19 +356,16 @@
     7.4  
     7.5  subsubsection {* Examples *}
     7.6  
     7.7 -text {* The following produces an example session as separate
     7.8 -  directory called @{verbatim Test}:
     7.9 +text {* Produce session @{verbatim Test} within a separate directory
    7.10 +  of the same name:
    7.11  \begin{ttbox}
    7.12 -isabelle mkroot Test && isabelle build -v -D Test
    7.13 +isabelle mkroot Test && isabelle build -D Test
    7.14  \end{ttbox}
    7.15  
    7.16 -  Option @{verbatim "-v"} is not required, but useful to reveal the
    7.17 -  the location of generated documents.
    7.18 -
    7.19 -  \medskip The subsequent example turns the current directory to a
    7.20 -  session directory with document and builds it:
    7.21 +  \medskip Upgrade the current directory into a session ROOT with
    7.22 +  document preparation, and build it:
    7.23  \begin{ttbox}
    7.24 -isabelle mkroot -d && isabelle build -D.
    7.25 +isabelle mkroot -d && isabelle build -D .
    7.26  \end{ttbox}
    7.27  *}
    7.28  
     8.1 --- a/doc-src/System/Thy/document/Interfaces.tex	Tue Aug 14 16:09:45 2012 +0200
     8.2 +++ b/doc-src/System/Thy/document/Interfaces.tex	Tue Aug 14 16:18:15 2012 +0200
     8.3 @@ -36,6 +36,7 @@
     8.4    Options are:
     8.5      -J OPTION    add JVM runtime option (default JEDIT_JAVA_OPTIONS)
     8.6      -b           build only
     8.7 +    -d DIR       include session directory
     8.8      -f           fresh build
     8.9      -j OPTION    add jEdit runtime option (default JEDIT_OPTIONS)
    8.10      -l NAME      logic image name (default ISABELLE_LOGIC)
    8.11 @@ -45,8 +46,12 @@
    8.12  (default Scratch.thy).
    8.13  \end{ttbox}
    8.14  
    8.15 -  The \verb|-l| option specifies the logic image.  The
    8.16 -  \verb|-m| option specifies additional print modes.
    8.17 +  The \verb|-l| option specifies the session name of the logic
    8.18 +  image to be used for proof processing.  Additional session root
    8.19 +  directories may be included via option \verb|-d| to augment
    8.20 +  that name space (see also \secref{sec:tool-build}).
    8.21 +
    8.22 +  The \verb|-m| option specifies additional print modes.
    8.23  
    8.24    The \verb|-J| and \verb|-j| options allow to pass
    8.25    additional low-level options to the JVM or jEdit, respectively.  The
     9.1 --- a/doc-src/System/Thy/document/Sessions.tex	Tue Aug 14 16:09:45 2012 +0200
     9.2 +++ b/doc-src/System/Thy/document/Sessions.tex	Tue Aug 14 16:18:15 2012 +0200
     9.3 @@ -471,19 +471,16 @@
     9.4  \isamarkuptrue%
     9.5  %
     9.6  \begin{isamarkuptext}%
     9.7 -The following produces an example session as separate
     9.8 -  directory called \verb|Test|:
     9.9 +Produce session \verb|Test| within a separate directory
    9.10 +  of the same name:
    9.11  \begin{ttbox}
    9.12 -isabelle mkroot Test && isabelle build -v -D Test
    9.13 +isabelle mkroot Test && isabelle build -D Test
    9.14  \end{ttbox}
    9.15  
    9.16 -  Option \verb|-v| is not required, but useful to reveal the
    9.17 -  the location of generated documents.
    9.18 -
    9.19 -  \medskip The subsequent example turns the current directory to a
    9.20 -  session directory with document and builds it:
    9.21 +  \medskip Upgrade the current directory into a session ROOT with
    9.22 +  document preparation, and build it:
    9.23  \begin{ttbox}
    9.24 -isabelle mkroot -d && isabelle build -D.
    9.25 +isabelle mkroot -d && isabelle build -D .
    9.26  \end{ttbox}%
    9.27  \end{isamarkuptext}%
    9.28  \isamarkuptrue%
    10.1 --- a/etc/components	Tue Aug 14 16:09:45 2012 +0200
    10.2 +++ b/etc/components	Tue Aug 14 16:18:15 2012 +0200
    10.3 @@ -10,6 +10,7 @@
    10.4  src/LCF
    10.5  src/Sequents
    10.6  #misc components
    10.7 +doc-src
    10.8  src/Tools/Code
    10.9  src/Tools/jEdit
   10.10  src/Tools/WWW_Find
    11.1 --- a/etc/options	Tue Aug 14 16:09:45 2012 +0200
    11.2 +++ b/etc/options	Tue Aug 14 16:18:15 2012 +0200
    11.3 @@ -1,68 +1,70 @@
    11.4  (* :mode=isabelle-options: *)
    11.5  
    11.6 -declare browser_info : bool = false
    11.7 +option browser_info : bool = false
    11.8    -- "generate theory browser information"
    11.9  
   11.10 -declare document : string = ""
   11.11 +option document : string = ""
   11.12    -- "build document in given format: pdf, dvi, dvi.gz, ps, ps.gz, or false"
   11.13 -declare document_variants : string = "outline=/proof,/ML"
   11.14 -  -- "declare alternative document variants (separated by colons)"
   11.15 -declare document_graph : bool = false
   11.16 +option document_output : string = ""
   11.17 +  -- "document output directory (default within $ISABELLE_BROWSER_INFO tree)"
   11.18 +option document_variants : string = "document"
   11.19 +  -- "option alternative document variants (separated by colons)"
   11.20 +option document_graph : bool = false
   11.21    -- "generate session graph image for document"
   11.22 -declare document_dump : string = ""
   11.23 +option document_dump : string = ""
   11.24    -- "dump generated document sources into given directory"
   11.25 -declare document_dump_mode : string = "all"
   11.26 +option document_dump_mode : string = "all"
   11.27    -- "specific document dump mode: all, tex, tex+sty"
   11.28  
   11.29 -declare threads : int = 0
   11.30 +option threads : int = 0
   11.31    -- "maximum number of worker threads for prover process (0 = hardware max.)"
   11.32 -declare threads_trace : int = 0
   11.33 +option threads_trace : int = 0
   11.34    -- "level of tracing information for multithreading"
   11.35 -declare parallel_proofs : int = 2
   11.36 +option parallel_proofs : int = 2
   11.37    -- "level of parallel proof checking: 0, 1, 2"
   11.38 -declare parallel_proofs_threshold : int = 100
   11.39 +option parallel_proofs_threshold : int = 100
   11.40    -- "threshold for sub-proof parallelization"
   11.41  
   11.42 -declare print_mode : string = ""
   11.43 +option print_mode : string = ""
   11.44    -- "additional print modes for prover output (separated by commas)"
   11.45  
   11.46 -declare proofs : int = 1
   11.47 +option proofs : int = 1
   11.48    -- "level of detail for proof objects: 0, 1, 2"
   11.49 -declare quick_and_dirty : bool = false
   11.50 +option quick_and_dirty : bool = false
   11.51    -- "if true then some tools will OMIT some proofs"
   11.52 -declare skip_proofs : bool = false
   11.53 +option skip_proofs : bool = false
   11.54    -- "skip over proofs"
   11.55  
   11.56 -declare condition : string = ""
   11.57 +option condition : string = ""
   11.58    -- "required environment variables for subsequent theories (separated by commas)"
   11.59  
   11.60 -declare show_question_marks : bool = true
   11.61 +option show_question_marks : bool = true
   11.62    -- "show leading question mark of schematic variables"
   11.63  
   11.64 -declare names_long : bool = false
   11.65 +option names_long : bool = false
   11.66    -- "show fully qualified names"
   11.67 -declare names_short : bool = false
   11.68 +option names_short : bool = false
   11.69    -- "show base names only"
   11.70 -declare names_unique : bool = true
   11.71 +option names_unique : bool = true
   11.72    -- "show partially qualified names, as required for unique name resolution"
   11.73  
   11.74 -declare pretty_margin : int = 76
   11.75 +option pretty_margin : int = 76
   11.76    -- "right margin / page width of pretty printer in Isabelle/ML"
   11.77  
   11.78 -declare thy_output_display : bool = false
   11.79 +option thy_output_display : bool = false
   11.80    -- "indicate output as multi-line display-style material"
   11.81 -declare thy_output_break : bool = false
   11.82 +option thy_output_break : bool = false
   11.83    -- "control line breaks in non-display material"
   11.84 -declare thy_output_quotes : bool = false
   11.85 +option thy_output_quotes : bool = false
   11.86    -- "indicate if the output should be enclosed in double quotes"
   11.87 -declare thy_output_indent : int = 0
   11.88 +option thy_output_indent : int = 0
   11.89    -- "indentation for pretty printing of display material"
   11.90 -declare thy_output_source : bool = false
   11.91 +option thy_output_source : bool = false
   11.92    -- "print original source text rather than internal representation"
   11.93  
   11.94 -declare timing : bool = false
   11.95 +option timing : bool = false
   11.96    -- "global timing of toplevel command execution and theory processing"
   11.97  
   11.98 -declare timeout : real = 0
   11.99 +option timeout : real = 0
  11.100    -- "timeout for session build job (seconds > 0)"
  11.101  
    12.1 --- a/lib/Tools/mkroot	Tue Aug 14 16:09:45 2012 +0200
    12.2 +++ b/lib/Tools/mkroot	Tue Aug 14 16:18:15 2012 +0200
    12.3 @@ -89,7 +89,7 @@
    12.4  if [ "$DOC" = true ]; then
    12.5    cat > "$DIR/ROOT" <<EOF
    12.6  session "$NAME" = "$ISABELLE_LOGIC" +
    12.7 -  options [document = $ISABELLE_DOC_FORMAT]
    12.8 +  options [document = $ISABELLE_DOC_FORMAT, document_output = "output"]
    12.9    theories [document = false]
   12.10      (* Foo Bar *)
   12.11    theories
   12.12 @@ -192,7 +192,7 @@
   12.13  
   12.14  Now use the following command line to build the session:
   12.15  
   12.16 -  isabelle build -v $OPT_DIR
   12.17 +  isabelle build $OPT_DIR
   12.18  
   12.19  EOF
   12.20  
    13.1 --- a/lib/scripts/getsettings	Tue Aug 14 16:09:45 2012 +0200
    13.2 +++ b/lib/scripts/getsettings	Tue Aug 14 16:18:15 2012 +0200
    13.3 @@ -197,7 +197,6 @@
    13.4  
    13.5  #main components
    13.6  init_component "$ISABELLE_HOME"
    13.7 -[ -d "$ISABELLE_HOME/doc-src" ] && init_component "$ISABELLE_HOME/doc-src"
    13.8  [ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin"
    13.9  [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
   13.10  
    14.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Aug 14 16:09:45 2012 +0200
    14.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Aug 14 16:18:15 2012 +0200
    14.3 @@ -75,7 +75,8 @@
    14.4      -> Toplevel.transition -> Toplevel.transition
    14.5    val print_prop: (string list * string) -> Toplevel.transition -> Toplevel.transition
    14.6    val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
    14.7 -  val print_type: (string list * string) -> Toplevel.transition -> Toplevel.transition
    14.8 +  val print_type: (string list * (string * string option)) ->
    14.9 +    Toplevel.transition -> Toplevel.transition
   14.10    val header_markup: Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
   14.11    val local_theory_markup: (xstring * Position.T) option * (Symbol_Pos.text * Position.T) ->
   14.12      Toplevel.transition -> Toplevel.transition
   14.13 @@ -494,9 +495,19 @@
   14.14          Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)])
   14.15    end;
   14.16  
   14.17 -fun string_of_type ctxt s =
   14.18 -  let val T = Syntax.read_typ ctxt s
   14.19 -  in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end;
   14.20 +fun string_of_type ctxt (s, NONE) =
   14.21 +      let val T = Syntax.read_typ ctxt s
   14.22 +      in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end
   14.23 +  | string_of_type ctxt (s1, SOME s2) =
   14.24 +      let
   14.25 +        val ctxt' = Config.put show_sorts true ctxt;
   14.26 +        val raw_T = Syntax.parse_typ ctxt' s1;
   14.27 +        val S = Syntax.read_sort ctxt' s2;
   14.28 +        val T =
   14.29 +          Syntax.check_term ctxt'
   14.30 +            (Logic.mk_type raw_T |> Type.constraint (Term.itselfT (Type_Infer.anyT S)))
   14.31 +          |> Logic.dest_type;
   14.32 +      in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt' T)) end;
   14.33  
   14.34  fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
   14.35    Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) ());
    15.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Aug 14 16:09:45 2012 +0200
    15.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Aug 14 16:18:15 2012 +0200
    15.3 @@ -902,7 +902,8 @@
    15.4  
    15.5  val _ =
    15.6    Outer_Syntax.improper_command @{command_spec "typ"} "read and print type"
    15.7 -    (opt_modes -- Parse.typ >> (Toplevel.no_timing oo Isar_Cmd.print_type));
    15.8 +    (opt_modes -- (Parse.typ -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort))
    15.9 +      >> (Toplevel.no_timing oo Isar_Cmd.print_type));
   15.10  
   15.11  val _ =
   15.12    Outer_Syntax.improper_command @{command_spec "print_codesetup"} "print code generator setup"
    16.1 --- a/src/Pure/PIDE/document.scala	Tue Aug 14 16:09:45 2012 +0200
    16.2 +++ b/src/Pure/PIDE/document.scala	Tue Aug 14 16:18:15 2012 +0200
    16.3 @@ -51,8 +51,9 @@
    16.4      object Name
    16.5      {
    16.6        val empty = Name("", "", "")
    16.7 -      def apply(path: Path): Name =
    16.8 +      def apply(raw_path: Path): Name =
    16.9        {
   16.10 +        val path = raw_path.expand
   16.11          val node = path.implode
   16.12          val dir = path.dir.implode
   16.13          val theory = Thy_Header.thy_name(node) getOrElse error("Bad theory file name: " + path)
    17.1 --- a/src/Pure/System/build.ML	Tue Aug 14 16:09:45 2012 +0200
    17.2 +++ b/src/Pure/System/build.ML	Tue Aug 14 16:18:15 2012 +0200
    17.3 @@ -65,12 +65,19 @@
    17.4                (pair string ((list (pair Options.decode (list string)))))))))
    17.5            end;
    17.6  
    17.7 +      val document_variants =
    17.8 +        map Present.read_variant (space_explode ":" (Options.string options "document_variants"));
    17.9 +      val _ =
   17.10 +        (case duplicates (op =) (map fst document_variants) of
   17.11 +          [] => ()
   17.12 +        | dups => error ("Duplicate document variants: " ^ commas_quote dups));
   17.13        val _ =
   17.14          Session.init do_output false
   17.15            (Options.bool options "browser_info") browser_info
   17.16            (Options.string options "document")
   17.17            (Options.bool options "document_graph")
   17.18 -          (space_explode ":" (Options.string options "document_variants"))
   17.19 +          (Options.string options "document_output")
   17.20 +          document_variants
   17.21            parent_name name
   17.22            (Options.string options "document_dump",
   17.23              Present.dump_mode (Options.string options "document_dump_mode"))
    18.1 --- a/src/Pure/System/build.scala	Tue Aug 14 16:09:45 2012 +0200
    18.2 +++ b/src/Pure/System/build.scala	Tue Aug 14 16:18:15 2012 +0200
    18.3 @@ -145,6 +145,8 @@
    18.4  
    18.5      def topological_order: List[(String, Session_Info)] =
    18.6        graph.topological_order.map(name => (name, apply(name)))
    18.7 +
    18.8 +    override def toString: String = graph.entries.map(_._1).toList.sorted.mkString(",")
    18.9    }
   18.10  
   18.11  
   18.12 @@ -309,7 +311,15 @@
   18.13    sealed case class Session_Content(
   18.14      loaded_theories: Set[String],
   18.15      syntax: Outer_Syntax,
   18.16 -    sources: List[(Path, SHA1.Digest)])
   18.17 +    sources: List[(Path, SHA1.Digest)],
   18.18 +    errors: List[String])
   18.19 +  {
   18.20 +    def check_errors: Session_Content =
   18.21 +    {
   18.22 +      if (errors.isEmpty) this
   18.23 +      else error(cat_lines(errors))
   18.24 +    }
   18.25 +  }
   18.26  
   18.27    sealed case class Deps(deps: Map[String, Session_Content])
   18.28    {
   18.29 @@ -321,16 +331,19 @@
   18.30    def dependencies(verbose: Boolean, tree: Session_Tree): Deps =
   18.31      Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
   18.32        { case (deps, (name, info)) =>
   18.33 -          val (preloaded, parent_syntax) =
   18.34 +          val (preloaded, parent_syntax, parent_errors) =
   18.35              info.parent match {
   18.36 -              case Some(parent) => (deps(parent).loaded_theories, deps(parent).syntax)
   18.37 +              case Some(parent_name) =>
   18.38 +                val parent = deps(parent_name)
   18.39 +                (parent.loaded_theories, parent.syntax, parent.errors)
   18.40                case None =>
   18.41 -                (Set.empty[String],
   18.42 +                val init_syntax =
   18.43                    Outer_Syntax.init() +
   18.44                      // FIXME avoid hardwired stuff!?
   18.45                      ("theory", Keyword.THY_BEGIN) +
   18.46                      ("hence", Keyword.PRF_ASM_GOAL, "then have") +
   18.47 -                    ("thus", Keyword.PRF_ASM_GOAL, "then show"))
   18.48 +                    ("thus", Keyword.PRF_ASM_GOAL, "then show")
   18.49 +                (Set.empty[String], init_syntax, Nil)
   18.50              }
   18.51            val thy_info = new Thy_Info(new Thy_Load(preloaded))
   18.52  
   18.53 @@ -362,17 +375,20 @@
   18.54                  error(msg + "\nThe error(s) above occurred in session " +
   18.55                    quote(name) + Position.str_of(info.pos))
   18.56              }
   18.57 +          val errors = parent_errors ::: thy_deps.map(d => d._2.errors).flatten
   18.58  
   18.59 -          deps + (name -> Session_Content(loaded_theories, syntax, sources))
   18.60 +          deps + (name -> Session_Content(loaded_theories, syntax, sources, errors))
   18.61        }))
   18.62  
   18.63 -  def session_content(session: String): Session_Content =
   18.64 +  def session_content(dirs: List[Path], session: String): Session_Content =
   18.65    {
   18.66 -    val (_, tree) = find_sessions(Options.init(), Nil).required(false, Nil, List(session))
   18.67 +    val (_, tree) =
   18.68 +      find_sessions(Options.init(), dirs.map((false, _))).required(false, Nil, List(session))
   18.69      dependencies(false, tree)(session)
   18.70    }
   18.71  
   18.72 -  def outer_syntax(session: String): Outer_Syntax = session_content(session).syntax
   18.73 +  def outer_syntax(session: String): Outer_Syntax =
   18.74 +    session_content(Nil, session).check_errors.syntax
   18.75  
   18.76  
   18.77    /* jobs */
    19.1 --- a/src/Pure/System/options.scala	Tue Aug 14 16:09:45 2012 +0200
    19.2 +++ b/src/Pure/System/options.scala	Tue Aug 14 16:18:15 2012 +0200
    19.3 @@ -30,12 +30,10 @@
    19.4  
    19.5    /* parsing */
    19.6  
    19.7 -  private val DECLARE = "declare"
    19.8 -  private val DEFINE = "define"
    19.9 +  private val OPTION = "option"
   19.10  
   19.11    lazy val options_syntax =
   19.12 -    Outer_Syntax.init() + ":" + "=" + "--" +
   19.13 -      (DECLARE, Keyword.THY_DECL) + (DEFINE, Keyword.PRF_DECL)
   19.14 +    Outer_Syntax.init() + ":" + "=" + "--" + (OPTION, Keyword.THY_DECL)
   19.15  
   19.16    private object Parser extends Parse.Parser
   19.17    {
   19.18 @@ -49,11 +47,9 @@
   19.19            { case s ~ n => if (s.isDefined) "-" + n else n } |
   19.20          atom("option value", tok => tok.is_name || tok.is_float)
   19.21  
   19.22 -      command(DECLARE) ~! (option_name ~ keyword(":") ~ option_type ~
   19.23 +      command(OPTION) ~! (option_name ~ keyword(":") ~ option_type ~
   19.24        keyword("=") ~ option_value ~ (keyword("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
   19.25 -        { case _ ~ (a ~ _ ~ b ~ _ ~ c ~ d) => (options: Options) => options.declare(a, b, c, d) } |
   19.26 -      command(DEFINE) ~! (option_name ~ keyword("=") ~ option_value) ^^
   19.27 -        { case _ ~ (a ~ _ ~ b) => (options: Options) => options.define(a, b) }
   19.28 +        { case _ ~ (a ~ _ ~ b ~ _ ~ c ~ d) => (options: Options) => options.declare(a, b, c, d) }
   19.29      }
   19.30  
   19.31      def parse_entries(file: Path): List[Options => Options] =
   19.32 @@ -114,7 +110,7 @@
   19.33  
   19.34    def print: String =
   19.35      cat_lines(options.toList.sortBy(_._1).map({ case (name, opt) =>
   19.36 -      name + " : " + opt.typ.print + " = " +
   19.37 +      "option " + name + " : " + opt.typ.print + " = " +
   19.38          (if (opt.typ == Options.String) quote(opt.value) else opt.value) +
   19.39        "\n  -- " + quote(opt.description) }))
   19.40  
    20.1 --- a/src/Pure/System/session.ML	Tue Aug 14 16:09:45 2012 +0200
    20.2 +++ b/src/Pure/System/session.ML	Tue Aug 14 16:18:15 2012 +0200
    20.3 @@ -10,7 +10,7 @@
    20.4    val name: unit -> string
    20.5    val welcome: unit -> string
    20.6    val finish: unit -> unit
    20.7 -  val init: bool -> bool -> bool -> string -> string -> bool -> string list ->
    20.8 +  val init: bool -> bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
    20.9      string -> string -> string * Present.dump_mode -> string -> bool -> unit
   20.10    val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b
   20.11    val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
   20.12 @@ -102,23 +102,28 @@
   20.13         remote_path := SOME (Url.explode rpath);
   20.14     (! remote_path, rpath <> ""));
   20.15  
   20.16 -fun init build reset info info_path doc doc_graph doc_variants parent name doc_dump rpath verbose =
   20.17 +fun init build reset info info_path doc doc_graph doc_output doc_variants
   20.18 +    parent name doc_dump rpath verbose =
   20.19   (init_name reset parent name;
   20.20 -  Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_variants
   20.21 -    (path ()) name doc_dump (get_rpath rpath) verbose
   20.22 +  Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_output
   20.23 +    doc_variants (path ()) name doc_dump (get_rpath rpath) verbose
   20.24      (map Thy_Info.get_theory (Thy_Info.get_names ())));
   20.25  
   20.26  local
   20.27  
   20.28  fun doc_dump (cp, dump) = (dump, if cp then Present.Dump_all else Present.Dump_tex_sty);
   20.29  
   20.30 +fun read_variants strs =
   20.31 +  rev (distinct (eq_fst (op =)) (rev (("document", "") :: map Present.read_variant strs)))
   20.32 +  |> filter_out (fn (_, s) => s = "-");
   20.33 +
   20.34  in
   20.35  
   20.36  fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
   20.37      name dump rpath level timing verbose max_threads trace_threads
   20.38      parallel_proofs parallel_proofs_threshold =
   20.39    ((fn () =>
   20.40 -     (init build reset info info_path doc doc_graph doc_variants parent name
   20.41 +     (init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name
   20.42          (doc_dump dump) rpath verbose;
   20.43        with_timing item timing use root;
   20.44        finish ()))
    21.1 --- a/src/Pure/System/session.scala	Tue Aug 14 16:09:45 2012 +0200
    21.2 +++ b/src/Pure/System/session.scala	Tue Aug 14 16:18:15 2012 +0200
    21.3 @@ -171,7 +171,7 @@
    21.4  
    21.5    /* actor messages */
    21.6  
    21.7 -  private case class Start(logic: String, args: List[String])
    21.8 +  private case class Start(dirs: List[Path], logic: String, args: List[String])
    21.9    private case object Cancel_Execution
   21.10    private case class Edit(edits: List[Document.Edit_Text])
   21.11    private case class Change(
   21.12 @@ -377,12 +377,12 @@
   21.13        receiveWithin(delay_commands_changed.flush_timeout) {
   21.14          case TIMEOUT => delay_commands_changed.flush()
   21.15  
   21.16 -        case Start(name, args) if prover.isEmpty =>
   21.17 +        case Start(dirs, name, args) if prover.isEmpty =>
   21.18            if (phase == Session.Inactive || phase == Session.Failed) {
   21.19              phase = Session.Startup
   21.20  
   21.21              // FIXME static init in main constructor
   21.22 -            val content = Build.session_content(name)
   21.23 +            val content = Build.session_content(dirs, name).check_errors
   21.24              thy_load.register_thys(content.loaded_theories)
   21.25              base_syntax = content.syntax
   21.26  
   21.27 @@ -440,7 +440,8 @@
   21.28  
   21.29    /* actions */
   21.30  
   21.31 -  def start(name: String, args: List[String]) { session_actor ! Start(name, args) }
   21.32 +  def start(dirs: List[Path], name: String, args: List[String])
   21.33 +  { session_actor ! Start(dirs, name, args) }
   21.34  
   21.35    def stop() { commands_changed_buffer !? Stop; change_parser !? Stop; session_actor !? Stop }
   21.36  
    22.1 --- a/src/Pure/Thy/present.ML	Tue Aug 14 16:09:45 2012 +0200
    22.2 +++ b/src/Pure/Thy/present.ML	Tue Aug 14 16:18:15 2012 +0200
    22.3 @@ -19,8 +19,9 @@
    22.4     path: string, parents: string list} list -> unit
    22.5    datatype dump_mode = Dump_all | Dump_tex | Dump_tex_sty
    22.6    val dump_mode: string -> dump_mode
    22.7 -  val init: bool -> bool -> string -> string -> bool -> string list -> string list ->
    22.8 -    string -> string * dump_mode -> Url.T option * bool -> bool ->
    22.9 +  val read_variant: string -> string * string
   22.10 +  val init: bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
   22.11 +    string list -> string -> string * dump_mode -> Url.T option * bool -> bool ->
   22.12      theory list -> unit  (*not thread-safe!*)
   22.13    val finish: unit -> unit  (*not thread-safe!*)
   22.14    val init_theory: string -> unit
   22.15 @@ -219,17 +220,17 @@
   22.16  
   22.17  type session_info =
   22.18    {name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
   22.19 -    info: bool, doc_format: string, doc_graph: bool, documents: (string * string) list,
   22.20 -    doc_dump: (string * dump_mode), remote_path: Url.T option, verbose: bool,
   22.21 -    readme: Path.T option};
   22.22 +    info: bool, doc_format: string, doc_graph: bool, doc_output: Path.T option,
   22.23 +    documents: (string * string) list, doc_dump: (string * dump_mode), remote_path: Url.T option,
   22.24 +    verbose: bool, readme: Path.T option};
   22.25  
   22.26  fun make_session_info
   22.27 -  (name, parent, session, path, html_prefix, info, doc_format, doc_graph, documents,
   22.28 -    doc_dump, remote_path, verbose, readme) =
   22.29 +  (name, parent, session, path, html_prefix, info, doc_format, doc_graph, doc_output,
   22.30 +    documents, doc_dump, remote_path, verbose, readme) =
   22.31    {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix,
   22.32 -    info = info, doc_format = doc_format, doc_graph = doc_graph, documents = documents,
   22.33 -    doc_dump = doc_dump, remote_path = remote_path, verbose = verbose,
   22.34 -    readme = readme}: session_info;
   22.35 +    info = info, doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output,
   22.36 +    documents = documents, doc_dump = doc_dump, remote_path = remote_path,
   22.37 +    verbose = verbose, readme = readme}: session_info;
   22.38  
   22.39  
   22.40  (* state *)
   22.41 @@ -274,16 +275,12 @@
   22.42    | [name, tags] => (name, tags)
   22.43    | _ => error ("Malformed document variant specification: " ^ quote str));
   22.44  
   22.45 -fun read_variants strs =
   22.46 -  rev (distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_variant strs)))
   22.47 -  |> filter_out (fn (_, s) => s = "-");
   22.48 -
   22.49  
   22.50  (* init session *)
   22.51  
   22.52  fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
   22.53  
   22.54 -fun init build info info_path doc doc_graph doc_variants path name
   22.55 +fun init build info info_path doc doc_graph document_output doc_variants path name
   22.56      (doc_dump as (dump_prefix, _)) (remote_path, first_time) verbose thys =
   22.57    if not build andalso not info andalso doc = "" andalso dump_prefix = "" then
   22.58      (browser_info := empty_browser_info; session_info := NONE)
   22.59 @@ -293,13 +290,14 @@
   22.60        val session_name = name_of_session path;
   22.61        val sess_prefix = Path.make path;
   22.62        val html_prefix = Path.append (Path.expand (Path.explode info_path)) sess_prefix;
   22.63 +      val doc_output = if document_output = "" then NONE else SOME (Path.explode document_output);
   22.64  
   22.65        val documents =
   22.66          if doc = "" then []
   22.67          else if not (can File.check_dir document_path) then
   22.68            (if verbose then Output.physical_stderr "Warning: missing document directory\n"
   22.69             else (); [])
   22.70 -        else read_variants doc_variants;
   22.71 +        else doc_variants;
   22.72  
   22.73        val parent_index_path = Path.append Path.parent index_path;
   22.74        val index_up_lnk =
   22.75 @@ -318,8 +316,8 @@
   22.76          (Url.File index_path, session_name) docs (Url.explode "medium.html");
   22.77      in
   22.78        session_info :=
   22.79 -        SOME (make_session_info (name, parent_name, session_name, path, html_prefix,
   22.80 -          info, doc, doc_graph, documents, doc_dump, remote_path, verbose, readme));
   22.81 +        SOME (make_session_info (name, parent_name, session_name, path, html_prefix, info, doc,
   22.82 +          doc_graph, doc_output, documents, doc_dump, remote_path, verbose, readme));
   22.83        browser_info := init_browser_info remote_path path thys;
   22.84        add_html_index (0, index_text)
   22.85      end;
   22.86 @@ -327,11 +325,11 @@
   22.87  
   22.88  (* isabelle tool wrappers *)
   22.89  
   22.90 -fun isabelle_document verbose format name tags path result_path =
   22.91 +fun isabelle_document {verbose, purge} format name tags dir =
   22.92    let
   22.93 -    val s = "\"$ISABELLE_TOOL\" document -c -o '" ^ format ^ "' \
   22.94 -      \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path path ^ " 2>&1";
   22.95 -    val doc_path = Path.append result_path (Path.ext format (Path.basic name));
   22.96 +    val s = "\"$ISABELLE_TOOL\" document" ^ (if purge then " -c" else "") ^ " -o '" ^ format ^ "' \
   22.97 +      \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path dir ^ " 2>&1";
   22.98 +    val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format];
   22.99      val _ = if verbose then writeln s else ();
  22.100      val (out, rc) = Isabelle_System.bash_output s;
  22.101      val _ =
  22.102 @@ -369,8 +367,8 @@
  22.103  
  22.104  
  22.105  fun finish () =
  22.106 -  session_default () (fn {name, info, html_prefix, doc_format,
  22.107 -    doc_graph, documents, doc_dump = (dump_prefix, dump_mode), path, verbose, readme, ...} =>
  22.108 +  session_default () (fn {name, info, html_prefix, doc_format, doc_graph, doc_output,
  22.109 +    documents, doc_dump = (dump_prefix, dump_mode), path, verbose, readme, ...} =>
  22.110    let
  22.111      val {theories, files, tex_index, html_index, graph} = ! browser_info;
  22.112      val thys = Symtab.dest theories;
  22.113 @@ -433,11 +431,19 @@
  22.114      val doc_paths =
  22.115        documents |> Par_List.map (fn (name, tags) =>
  22.116          let
  22.117 -          val path = Path.append html_prefix (Path.basic name);
  22.118 -          val _ = prepare_sources path Dump_all;
  22.119 -        in isabelle_document true doc_format name tags path html_prefix end);
  22.120 +          val (doc_prefix, purge) =
  22.121 +            (case doc_output of
  22.122 +              SOME path => (path, false)
  22.123 +            | NONE => (html_prefix, true));
  22.124 +          val _ =
  22.125 +            File.eq (document_path, doc_prefix) andalso
  22.126 +              error ("Overlap of document input and output directory " ^ Path.print doc_prefix);
  22.127 +          val dir = Path.append doc_prefix (Path.basic name);
  22.128 +          val mode = if File.eq (document_path, dir) then Dump_tex_sty else Dump_all;
  22.129 +          val _ = prepare_sources dir mode;
  22.130 +        in isabelle_document {verbose = true, purge = purge} doc_format name tags dir end);
  22.131      val _ =
  22.132 -      if verbose then
  22.133 +      if verbose orelse is_some doc_output then
  22.134          doc_paths
  22.135          |> List.app (fn doc => Output.physical_stderr ("Document at " ^ show_path doc ^ "\n"))
  22.136        else ();
  22.137 @@ -543,7 +549,8 @@
  22.138        |> File.write (Path.append doc_path (tex_path name)));
  22.139      val _ = write_tex_index tex_index doc_path;
  22.140  
  22.141 -    val result = isabelle_document false doc_format documentN "" doc_path dir;
  22.142 +    val result =
  22.143 +      isabelle_document {verbose = false, purge = true} doc_format documentN "" doc_path;
  22.144      val result' = Isabelle_System.create_tmp_path documentN doc_format;
  22.145      val _ = File.copy result result';
  22.146    in result' end);
    23.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Tue Aug 14 16:09:45 2012 +0200
    23.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Tue Aug 14 16:18:15 2012 +0200
    23.3 @@ -52,6 +52,7 @@
    23.4    echo "    -J OPTION    add JVM runtime option"
    23.5    echo "                 (default JEDIT_JAVA_OPTIONS=$JEDIT_JAVA_OPTIONS)"
    23.6    echo "    -b           build only"
    23.7 +  echo "    -d DIR       include session directory"
    23.8    echo "    -f           fresh build"
    23.9    echo "    -j OPTION    add jEdit runtime option"
   23.10    echo "                 (default JEDIT_OPTIONS=$JEDIT_OPTIONS)"
   23.11 @@ -82,13 +83,14 @@
   23.12  
   23.13  BUILD_ONLY=false
   23.14  BUILD_JARS="jars"
   23.15 +JEDIT_SESSION_DIRS=""
   23.16  JEDIT_LOGIC="$ISABELLE_LOGIC"
   23.17  JEDIT_PRINT_MODE=""
   23.18  
   23.19  function getoptions()
   23.20  {
   23.21    OPTIND=1
   23.22 -  while getopts "J:bdfj:l:m:" OPT
   23.23 +  while getopts "J:bd:fj:l:m:" OPT
   23.24    do
   23.25      case "$OPT" in
   23.26        J)
   23.27 @@ -97,6 +99,13 @@
   23.28        b)
   23.29          BUILD_ONLY=true
   23.30          ;;
   23.31 +      d)
   23.32 +        if [ -z "$JEDIT_SESSION_DIRS" ]; then
   23.33 +          JEDIT_SESSION_DIRS="$OPTARG"
   23.34 +        else
   23.35 +          JEDIT_SESSION_DIRS="$JEDIT_SESSION_DIRS:$OPTARG"
   23.36 +        fi
   23.37 +        ;;
   23.38        f)
   23.39          BUILD_JARS="jars_fresh"
   23.40          ;;
   23.41 @@ -283,7 +292,7 @@
   23.42        ;;
   23.43    esac
   23.44  
   23.45 -  export JEDIT_LOGIC JEDIT_PRINT_MODE
   23.46 +  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE
   23.47  
   23.48    exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \
   23.49      -jar "$(jvmpath "$JEDIT_HOME/dist/jedit.jar")" \
    24.1 --- a/src/Tools/jEdit/src/plugin.scala	Tue Aug 14 16:09:45 2012 +0200
    24.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 14 16:18:15 2012 +0200
    24.3 @@ -300,6 +300,7 @@
    24.4  
    24.5    def start_session()
    24.6    {
    24.7 +    val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
    24.8      val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
    24.9      val logic = {
   24.10        val logic = Property("logic")
   24.11 @@ -307,7 +308,7 @@
   24.12        else Isabelle.default_logic()
   24.13      }
   24.14      val name = Path.explode(logic).base.implode  // FIXME more robust session name
   24.15 -    session.start(name, modes ::: List(logic))
   24.16 +    session.start(dirs, name, modes ::: List(logic))
   24.17    }
   24.18  
   24.19