--- a/Admin/Release/makedist Tue Aug 14 16:09:45 2012 +0200
+++ b/Admin/Release/makedist Tue Aug 14 16:18:15 2012 +0200
@@ -23,7 +23,6 @@
Usage: $PRG [OPTIONS] [VERSION]
Options are:
- -D retain doc-src component
-j JEDIT_BUILD build Isabelle/jEdit via given jedit_build component
-r RELEASE proper release with name"
@@ -47,16 +46,12 @@
# options
-RETAIN_DOC_SRC=""
RELEASE=""
ISABELLE_JEDIT_BUILD_HOME=""
-while getopts "Dj:r:" OPT
+while getopts "j:r:" OPT
do
case "$OPT" in
- D)
- RETAIN_DOC_SRC=true
- ;;
j)
ISABELLE_JEDIT_BUILD_HOME="$OPTARG"
;;
@@ -152,9 +147,7 @@
perl -pi -e 's/^(ISABELLE_SCALA_BUILD_OPTIONS=")/$1-optimise /,' etc/settings
-if [ -n "$RETAIN_DOC_SRC" ]; then
- cp -a doc-src doc-src.orig
-fi
+cp -a doc-src doc-src.orig
./Admin/build all || fail "Failed to build distribution"
@@ -174,9 +167,7 @@
rm doc/adaptation.dvi doc/adaptation.pdf doc/architecture.dvi doc/architecture.pdf
rm -rf doc-src
-if [ -n "$RETAIN_DOC_SRC" ]; then
- mv doc-src.orig doc-src
-fi
+mv doc-src.orig doc-src
mkdir -p contrib
cat >contrib/README <<EOF
--- a/Admin/isatest/isatest-makedist Tue Aug 14 16:09:45 2012 +0200
+++ b/Admin/isatest/isatest-makedist Tue Aug 14 16:18:15 2012 +0200
@@ -60,7 +60,7 @@
echo "### building distribution" >> $DISTLOG 2>&1
mkdir -p $DISTPREFIX
-$MAKEDIST -D -j "/home/isabelle/contrib_devel/jedit_build-20120414" >> $DISTLOG 2>&1
+$MAKEDIST -j "/home/isabelle/contrib_devel/jedit_build-20120414" >> $DISTLOG 2>&1
if [ $? -ne 0 ]
then
--- a/NEWS Tue Aug 14 16:09:45 2012 +0200
+++ b/NEWS Tue Aug 14 16:18:15 2012 +0200
@@ -29,6 +29,12 @@
operators like COMP, INCR_COMP, COMP_INCR, which need to be applied
with some care where this is really required.
+* Command 'typ' supports an additional variant with explicit sort
+constraint, to infer and check the most general type conforming to a
+given given sort. Example (in HOL):
+
+ typ "_ * _ * bool * unit" :: finite
+
*** HOL ***
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Tue Aug 14 16:09:45 2012 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Tue Aug 14 16:18:15 2012 +0200
@@ -47,7 +47,7 @@
internal logical entities in a human-readable fashion.
@{rail "
- @@{command typ} @{syntax modes}? @{syntax type}
+ @@{command typ} @{syntax modes}? @{syntax type} ('::' @{syntax sort})?
;
@@{command term} @{syntax modes}? @{syntax term}
;
@@ -65,8 +65,15 @@
\begin{description}
- \item @{command "typ"}~@{text \<tau>} reads and prints types of the
- meta-logic according to the current theory or proof context.
+ \item @{command "typ"}~@{text \<tau>} reads and prints a type expression
+ according to the current context.
+
+ \item @{command "typ"}~@{text "\<tau> :: s"} uses type-inference to
+ determine the most general way to make @{text "\<tau>"} conform to sort
+ @{text "s"}. For concrete @{text "\<tau>"} this checks if the type
+ belongs to that sort. Dummy type parameters ``@{text "_"}''
+ (underscore) are assigned to fresh type variables with most general
+ sorts, according the the principles of type-inference.
\item @{command "term"}~@{text t} and @{command "prop"}~@{text \<phi>}
read, type-check and print terms or propositions according to the
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Tue Aug 14 16:09:45 2012 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Tue Aug 14 16:18:15 2012 +0200
@@ -75,6 +75,11 @@
\rail@nont{\hyperlink{syntax.modes}{\mbox{\isa{modes}}}}[]
\rail@endbar
\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
+\rail@nont{\hyperlink{syntax.sort}{\mbox{\isa{sort}}}}[]
+\rail@endbar
\rail@end
\rail@begin{2}{}
\rail@term{\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}}[]
@@ -139,8 +144,15 @@
\begin{description}
- \item \hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}~\isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} reads and prints types of the
- meta-logic according to the current theory or proof context.
+ \item \hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}~\isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} reads and prints a type expression
+ according to the current context.
+
+ \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
+ determine the most general way to make \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} conform to sort
+ \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
+ belongs to that sort. Dummy type parameters ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}}''
+ (underscore) are assigned to fresh type variables with most general
+ sorts, according the the principles of type-inference.
\item \hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}~\isa{t} and \hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}~\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}}
read, type-check and print terms or propositions according to the
--- a/doc-src/System/Thy/Interfaces.thy Tue Aug 14 16:09:45 2012 +0200
+++ b/doc-src/System/Thy/Interfaces.thy Tue Aug 14 16:18:15 2012 +0200
@@ -15,6 +15,7 @@
Options are:
-J OPTION add JVM runtime option (default JEDIT_JAVA_OPTIONS)
-b build only
+ -d DIR include session directory
-f fresh build
-j OPTION add jEdit runtime option (default JEDIT_OPTIONS)
-l NAME logic image name (default ISABELLE_LOGIC)
@@ -24,8 +25,12 @@
(default Scratch.thy).
\end{ttbox}
- The @{verbatim "-l"} option specifies the logic image. The
- @{verbatim "-m"} option specifies additional print modes.
+ The @{verbatim "-l"} option specifies the session name of the logic
+ image to be used for proof processing. Additional session root
+ directories may be included via option @{verbatim "-d"} to augment
+ that name space (see also \secref{sec:tool-build}).
+
+ The @{verbatim "-m"} option specifies additional print modes.
The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass
additional low-level options to the JVM or jEdit, respectively. The
--- a/doc-src/System/Thy/Sessions.thy Tue Aug 14 16:09:45 2012 +0200
+++ b/doc-src/System/Thy/Sessions.thy Tue Aug 14 16:18:15 2012 +0200
@@ -356,19 +356,16 @@
subsubsection {* Examples *}
-text {* The following produces an example session as separate
- directory called @{verbatim Test}:
+text {* Produce session @{verbatim Test} within a separate directory
+ of the same name:
\begin{ttbox}
-isabelle mkroot Test && isabelle build -v -D Test
+isabelle mkroot Test && isabelle build -D Test
\end{ttbox}
- Option @{verbatim "-v"} is not required, but useful to reveal the
- the location of generated documents.
-
- \medskip The subsequent example turns the current directory to a
- session directory with document and builds it:
+ \medskip Upgrade the current directory into a session ROOT with
+ document preparation, and build it:
\begin{ttbox}
-isabelle mkroot -d && isabelle build -D.
+isabelle mkroot -d && isabelle build -D .
\end{ttbox}
*}
--- a/doc-src/System/Thy/document/Interfaces.tex Tue Aug 14 16:09:45 2012 +0200
+++ b/doc-src/System/Thy/document/Interfaces.tex Tue Aug 14 16:18:15 2012 +0200
@@ -36,6 +36,7 @@
Options are:
-J OPTION add JVM runtime option (default JEDIT_JAVA_OPTIONS)
-b build only
+ -d DIR include session directory
-f fresh build
-j OPTION add jEdit runtime option (default JEDIT_OPTIONS)
-l NAME logic image name (default ISABELLE_LOGIC)
@@ -45,8 +46,12 @@
(default Scratch.thy).
\end{ttbox}
- The \verb|-l| option specifies the logic image. The
- \verb|-m| option specifies additional print modes.
+ The \verb|-l| option specifies the session name of the logic
+ image to be used for proof processing. Additional session root
+ directories may be included via option \verb|-d| to augment
+ that name space (see also \secref{sec:tool-build}).
+
+ The \verb|-m| option specifies additional print modes.
The \verb|-J| and \verb|-j| options allow to pass
additional low-level options to the JVM or jEdit, respectively. The
--- a/doc-src/System/Thy/document/Sessions.tex Tue Aug 14 16:09:45 2012 +0200
+++ b/doc-src/System/Thy/document/Sessions.tex Tue Aug 14 16:18:15 2012 +0200
@@ -471,19 +471,16 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The following produces an example session as separate
- directory called \verb|Test|:
+Produce session \verb|Test| within a separate directory
+ of the same name:
\begin{ttbox}
-isabelle mkroot Test && isabelle build -v -D Test
+isabelle mkroot Test && isabelle build -D Test
\end{ttbox}
- Option \verb|-v| is not required, but useful to reveal the
- the location of generated documents.
-
- \medskip The subsequent example turns the current directory to a
- session directory with document and builds it:
+ \medskip Upgrade the current directory into a session ROOT with
+ document preparation, and build it:
\begin{ttbox}
-isabelle mkroot -d && isabelle build -D.
+isabelle mkroot -d && isabelle build -D .
\end{ttbox}%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/etc/components Tue Aug 14 16:09:45 2012 +0200
+++ b/etc/components Tue Aug 14 16:18:15 2012 +0200
@@ -10,6 +10,7 @@
src/LCF
src/Sequents
#misc components
+doc-src
src/Tools/Code
src/Tools/jEdit
src/Tools/WWW_Find
--- a/etc/options Tue Aug 14 16:09:45 2012 +0200
+++ b/etc/options Tue Aug 14 16:18:15 2012 +0200
@@ -1,68 +1,70 @@
(* :mode=isabelle-options: *)
-declare browser_info : bool = false
+option browser_info : bool = false
-- "generate theory browser information"
-declare document : string = ""
+option document : string = ""
-- "build document in given format: pdf, dvi, dvi.gz, ps, ps.gz, or false"
-declare document_variants : string = "outline=/proof,/ML"
- -- "declare alternative document variants (separated by colons)"
-declare document_graph : bool = false
+option document_output : string = ""
+ -- "document output directory (default within $ISABELLE_BROWSER_INFO tree)"
+option document_variants : string = "document"
+ -- "option alternative document variants (separated by colons)"
+option document_graph : bool = false
-- "generate session graph image for document"
-declare document_dump : string = ""
+option document_dump : string = ""
-- "dump generated document sources into given directory"
-declare document_dump_mode : string = "all"
+option document_dump_mode : string = "all"
-- "specific document dump mode: all, tex, tex+sty"
-declare threads : int = 0
+option threads : int = 0
-- "maximum number of worker threads for prover process (0 = hardware max.)"
-declare threads_trace : int = 0
+option threads_trace : int = 0
-- "level of tracing information for multithreading"
-declare parallel_proofs : int = 2
+option parallel_proofs : int = 2
-- "level of parallel proof checking: 0, 1, 2"
-declare parallel_proofs_threshold : int = 100
+option parallel_proofs_threshold : int = 100
-- "threshold for sub-proof parallelization"
-declare print_mode : string = ""
+option print_mode : string = ""
-- "additional print modes for prover output (separated by commas)"
-declare proofs : int = 1
+option proofs : int = 1
-- "level of detail for proof objects: 0, 1, 2"
-declare quick_and_dirty : bool = false
+option quick_and_dirty : bool = false
-- "if true then some tools will OMIT some proofs"
-declare skip_proofs : bool = false
+option skip_proofs : bool = false
-- "skip over proofs"
-declare condition : string = ""
+option condition : string = ""
-- "required environment variables for subsequent theories (separated by commas)"
-declare show_question_marks : bool = true
+option show_question_marks : bool = true
-- "show leading question mark of schematic variables"
-declare names_long : bool = false
+option names_long : bool = false
-- "show fully qualified names"
-declare names_short : bool = false
+option names_short : bool = false
-- "show base names only"
-declare names_unique : bool = true
+option names_unique : bool = true
-- "show partially qualified names, as required for unique name resolution"
-declare pretty_margin : int = 76
+option pretty_margin : int = 76
-- "right margin / page width of pretty printer in Isabelle/ML"
-declare thy_output_display : bool = false
+option thy_output_display : bool = false
-- "indicate output as multi-line display-style material"
-declare thy_output_break : bool = false
+option thy_output_break : bool = false
-- "control line breaks in non-display material"
-declare thy_output_quotes : bool = false
+option thy_output_quotes : bool = false
-- "indicate if the output should be enclosed in double quotes"
-declare thy_output_indent : int = 0
+option thy_output_indent : int = 0
-- "indentation for pretty printing of display material"
-declare thy_output_source : bool = false
+option thy_output_source : bool = false
-- "print original source text rather than internal representation"
-declare timing : bool = false
+option timing : bool = false
-- "global timing of toplevel command execution and theory processing"
-declare timeout : real = 0
+option timeout : real = 0
-- "timeout for session build job (seconds > 0)"
--- a/lib/Tools/mkroot Tue Aug 14 16:09:45 2012 +0200
+++ b/lib/Tools/mkroot Tue Aug 14 16:18:15 2012 +0200
@@ -89,7 +89,7 @@
if [ "$DOC" = true ]; then
cat > "$DIR/ROOT" <<EOF
session "$NAME" = "$ISABELLE_LOGIC" +
- options [document = $ISABELLE_DOC_FORMAT]
+ options [document = $ISABELLE_DOC_FORMAT, document_output = "output"]
theories [document = false]
(* Foo Bar *)
theories
@@ -192,7 +192,7 @@
Now use the following command line to build the session:
- isabelle build -v $OPT_DIR
+ isabelle build $OPT_DIR
EOF
--- a/lib/scripts/getsettings Tue Aug 14 16:09:45 2012 +0200
+++ b/lib/scripts/getsettings Tue Aug 14 16:18:15 2012 +0200
@@ -197,7 +197,6 @@
#main components
init_component "$ISABELLE_HOME"
-[ -d "$ISABELLE_HOME/doc-src" ] && init_component "$ISABELLE_HOME/doc-src"
[ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin"
[ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
--- a/src/Pure/Isar/isar_cmd.ML Tue Aug 14 16:09:45 2012 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Tue Aug 14 16:18:15 2012 +0200
@@ -75,7 +75,8 @@
-> Toplevel.transition -> Toplevel.transition
val print_prop: (string list * string) -> Toplevel.transition -> Toplevel.transition
val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
- val print_type: (string list * string) -> Toplevel.transition -> Toplevel.transition
+ val print_type: (string list * (string * string option)) ->
+ Toplevel.transition -> Toplevel.transition
val header_markup: Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
val local_theory_markup: (xstring * Position.T) option * (Symbol_Pos.text * Position.T) ->
Toplevel.transition -> Toplevel.transition
@@ -494,9 +495,19 @@
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)])
end;
-fun string_of_type ctxt s =
- let val T = Syntax.read_typ ctxt s
- in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end;
+fun string_of_type ctxt (s, NONE) =
+ let val T = Syntax.read_typ ctxt s
+ in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end
+ | string_of_type ctxt (s1, SOME s2) =
+ let
+ val ctxt' = Config.put show_sorts true ctxt;
+ val raw_T = Syntax.parse_typ ctxt' s1;
+ val S = Syntax.read_sort ctxt' s2;
+ val T =
+ Syntax.check_term ctxt'
+ (Logic.mk_type raw_T |> Type.constraint (Term.itselfT (Type_Infer.anyT S)))
+ |> Logic.dest_type;
+ in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt' T)) end;
fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) ());
--- a/src/Pure/Isar/isar_syn.ML Tue Aug 14 16:09:45 2012 +0200
+++ b/src/Pure/Isar/isar_syn.ML Tue Aug 14 16:18:15 2012 +0200
@@ -902,7 +902,8 @@
val _ =
Outer_Syntax.improper_command @{command_spec "typ"} "read and print type"
- (opt_modes -- Parse.typ >> (Toplevel.no_timing oo Isar_Cmd.print_type));
+ (opt_modes -- (Parse.typ -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort))
+ >> (Toplevel.no_timing oo Isar_Cmd.print_type));
val _ =
Outer_Syntax.improper_command @{command_spec "print_codesetup"} "print code generator setup"
--- a/src/Pure/PIDE/document.scala Tue Aug 14 16:09:45 2012 +0200
+++ b/src/Pure/PIDE/document.scala Tue Aug 14 16:18:15 2012 +0200
@@ -51,8 +51,9 @@
object Name
{
val empty = Name("", "", "")
- def apply(path: Path): Name =
+ def apply(raw_path: Path): Name =
{
+ val path = raw_path.expand
val node = path.implode
val dir = path.dir.implode
val theory = Thy_Header.thy_name(node) getOrElse error("Bad theory file name: " + path)
--- a/src/Pure/System/build.ML Tue Aug 14 16:09:45 2012 +0200
+++ b/src/Pure/System/build.ML Tue Aug 14 16:18:15 2012 +0200
@@ -65,12 +65,19 @@
(pair string ((list (pair Options.decode (list string)))))))))
end;
+ val document_variants =
+ map Present.read_variant (space_explode ":" (Options.string options "document_variants"));
+ val _ =
+ (case duplicates (op =) (map fst document_variants) of
+ [] => ()
+ | dups => error ("Duplicate document variants: " ^ commas_quote dups));
val _ =
Session.init do_output false
(Options.bool options "browser_info") browser_info
(Options.string options "document")
(Options.bool options "document_graph")
- (space_explode ":" (Options.string options "document_variants"))
+ (Options.string options "document_output")
+ document_variants
parent_name name
(Options.string options "document_dump",
Present.dump_mode (Options.string options "document_dump_mode"))
--- a/src/Pure/System/build.scala Tue Aug 14 16:09:45 2012 +0200
+++ b/src/Pure/System/build.scala Tue Aug 14 16:18:15 2012 +0200
@@ -145,6 +145,8 @@
def topological_order: List[(String, Session_Info)] =
graph.topological_order.map(name => (name, apply(name)))
+
+ override def toString: String = graph.entries.map(_._1).toList.sorted.mkString(",")
}
@@ -309,7 +311,15 @@
sealed case class Session_Content(
loaded_theories: Set[String],
syntax: Outer_Syntax,
- sources: List[(Path, SHA1.Digest)])
+ sources: List[(Path, SHA1.Digest)],
+ errors: List[String])
+ {
+ def check_errors: Session_Content =
+ {
+ if (errors.isEmpty) this
+ else error(cat_lines(errors))
+ }
+ }
sealed case class Deps(deps: Map[String, Session_Content])
{
@@ -321,16 +331,19 @@
def dependencies(verbose: Boolean, tree: Session_Tree): Deps =
Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
{ case (deps, (name, info)) =>
- val (preloaded, parent_syntax) =
+ val (preloaded, parent_syntax, parent_errors) =
info.parent match {
- case Some(parent) => (deps(parent).loaded_theories, deps(parent).syntax)
+ case Some(parent_name) =>
+ val parent = deps(parent_name)
+ (parent.loaded_theories, parent.syntax, parent.errors)
case None =>
- (Set.empty[String],
+ val init_syntax =
Outer_Syntax.init() +
// FIXME avoid hardwired stuff!?
("theory", Keyword.THY_BEGIN) +
("hence", Keyword.PRF_ASM_GOAL, "then have") +
- ("thus", Keyword.PRF_ASM_GOAL, "then show"))
+ ("thus", Keyword.PRF_ASM_GOAL, "then show")
+ (Set.empty[String], init_syntax, Nil)
}
val thy_info = new Thy_Info(new Thy_Load(preloaded))
@@ -362,17 +375,20 @@
error(msg + "\nThe error(s) above occurred in session " +
quote(name) + Position.str_of(info.pos))
}
+ val errors = parent_errors ::: thy_deps.map(d => d._2.errors).flatten
- deps + (name -> Session_Content(loaded_theories, syntax, sources))
+ deps + (name -> Session_Content(loaded_theories, syntax, sources, errors))
}))
- def session_content(session: String): Session_Content =
+ def session_content(dirs: List[Path], session: String): Session_Content =
{
- val (_, tree) = find_sessions(Options.init(), Nil).required(false, Nil, List(session))
+ val (_, tree) =
+ find_sessions(Options.init(), dirs.map((false, _))).required(false, Nil, List(session))
dependencies(false, tree)(session)
}
- def outer_syntax(session: String): Outer_Syntax = session_content(session).syntax
+ def outer_syntax(session: String): Outer_Syntax =
+ session_content(Nil, session).check_errors.syntax
/* jobs */
--- a/src/Pure/System/options.scala Tue Aug 14 16:09:45 2012 +0200
+++ b/src/Pure/System/options.scala Tue Aug 14 16:18:15 2012 +0200
@@ -30,12 +30,10 @@
/* parsing */
- private val DECLARE = "declare"
- private val DEFINE = "define"
+ private val OPTION = "option"
lazy val options_syntax =
- Outer_Syntax.init() + ":" + "=" + "--" +
- (DECLARE, Keyword.THY_DECL) + (DEFINE, Keyword.PRF_DECL)
+ Outer_Syntax.init() + ":" + "=" + "--" + (OPTION, Keyword.THY_DECL)
private object Parser extends Parse.Parser
{
@@ -49,11 +47,9 @@
{ case s ~ n => if (s.isDefined) "-" + n else n } |
atom("option value", tok => tok.is_name || tok.is_float)
- command(DECLARE) ~! (option_name ~ keyword(":") ~ option_type ~
+ command(OPTION) ~! (option_name ~ keyword(":") ~ option_type ~
keyword("=") ~ option_value ~ (keyword("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
- { case _ ~ (a ~ _ ~ b ~ _ ~ c ~ d) => (options: Options) => options.declare(a, b, c, d) } |
- command(DEFINE) ~! (option_name ~ keyword("=") ~ option_value) ^^
- { case _ ~ (a ~ _ ~ b) => (options: Options) => options.define(a, b) }
+ { case _ ~ (a ~ _ ~ b ~ _ ~ c ~ d) => (options: Options) => options.declare(a, b, c, d) }
}
def parse_entries(file: Path): List[Options => Options] =
@@ -114,7 +110,7 @@
def print: String =
cat_lines(options.toList.sortBy(_._1).map({ case (name, opt) =>
- name + " : " + opt.typ.print + " = " +
+ "option " + name + " : " + opt.typ.print + " = " +
(if (opt.typ == Options.String) quote(opt.value) else opt.value) +
"\n -- " + quote(opt.description) }))
--- a/src/Pure/System/session.ML Tue Aug 14 16:09:45 2012 +0200
+++ b/src/Pure/System/session.ML Tue Aug 14 16:18:15 2012 +0200
@@ -10,7 +10,7 @@
val name: unit -> string
val welcome: unit -> string
val finish: unit -> unit
- val init: bool -> bool -> bool -> string -> string -> bool -> string list ->
+ val init: bool -> bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
string -> string -> string * Present.dump_mode -> string -> bool -> unit
val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b
val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
@@ -102,23 +102,28 @@
remote_path := SOME (Url.explode rpath);
(! remote_path, rpath <> ""));
-fun init build reset info info_path doc doc_graph doc_variants parent name doc_dump rpath verbose =
+fun init build reset info info_path doc doc_graph doc_output doc_variants
+ parent name doc_dump rpath verbose =
(init_name reset parent name;
- Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_variants
- (path ()) name doc_dump (get_rpath rpath) verbose
+ Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_output
+ doc_variants (path ()) name doc_dump (get_rpath rpath) verbose
(map Thy_Info.get_theory (Thy_Info.get_names ())));
local
fun doc_dump (cp, dump) = (dump, if cp then Present.Dump_all else Present.Dump_tex_sty);
+fun read_variants strs =
+ rev (distinct (eq_fst (op =)) (rev (("document", "") :: map Present.read_variant strs)))
+ |> filter_out (fn (_, s) => s = "-");
+
in
fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
name dump rpath level timing verbose max_threads trace_threads
parallel_proofs parallel_proofs_threshold =
((fn () =>
- (init build reset info info_path doc doc_graph doc_variants parent name
+ (init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name
(doc_dump dump) rpath verbose;
with_timing item timing use root;
finish ()))
--- a/src/Pure/System/session.scala Tue Aug 14 16:09:45 2012 +0200
+++ b/src/Pure/System/session.scala Tue Aug 14 16:18:15 2012 +0200
@@ -171,7 +171,7 @@
/* actor messages */
- private case class Start(logic: String, args: List[String])
+ private case class Start(dirs: List[Path], logic: String, args: List[String])
private case object Cancel_Execution
private case class Edit(edits: List[Document.Edit_Text])
private case class Change(
@@ -377,12 +377,12 @@
receiveWithin(delay_commands_changed.flush_timeout) {
case TIMEOUT => delay_commands_changed.flush()
- case Start(name, args) if prover.isEmpty =>
+ case Start(dirs, name, args) if prover.isEmpty =>
if (phase == Session.Inactive || phase == Session.Failed) {
phase = Session.Startup
// FIXME static init in main constructor
- val content = Build.session_content(name)
+ val content = Build.session_content(dirs, name).check_errors
thy_load.register_thys(content.loaded_theories)
base_syntax = content.syntax
@@ -440,7 +440,8 @@
/* actions */
- def start(name: String, args: List[String]) { session_actor ! Start(name, args) }
+ def start(dirs: List[Path], name: String, args: List[String])
+ { session_actor ! Start(dirs, name, args) }
def stop() { commands_changed_buffer !? Stop; change_parser !? Stop; session_actor !? Stop }
--- a/src/Pure/Thy/present.ML Tue Aug 14 16:09:45 2012 +0200
+++ b/src/Pure/Thy/present.ML Tue Aug 14 16:18:15 2012 +0200
@@ -19,8 +19,9 @@
path: string, parents: string list} list -> unit
datatype dump_mode = Dump_all | Dump_tex | Dump_tex_sty
val dump_mode: string -> dump_mode
- val init: bool -> bool -> string -> string -> bool -> string list -> string list ->
- string -> string * dump_mode -> Url.T option * bool -> bool ->
+ val read_variant: string -> string * string
+ val init: bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
+ string list -> string -> string * dump_mode -> Url.T option * bool -> bool ->
theory list -> unit (*not thread-safe!*)
val finish: unit -> unit (*not thread-safe!*)
val init_theory: string -> unit
@@ -219,17 +220,17 @@
type session_info =
{name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
- info: bool, doc_format: string, doc_graph: bool, documents: (string * string) list,
- doc_dump: (string * dump_mode), remote_path: Url.T option, verbose: bool,
- readme: Path.T option};
+ info: bool, doc_format: string, doc_graph: bool, doc_output: Path.T option,
+ documents: (string * string) list, doc_dump: (string * dump_mode), remote_path: Url.T option,
+ verbose: bool, readme: Path.T option};
fun make_session_info
- (name, parent, session, path, html_prefix, info, doc_format, doc_graph, documents,
- doc_dump, remote_path, verbose, readme) =
+ (name, parent, session, path, html_prefix, info, doc_format, doc_graph, doc_output,
+ documents, doc_dump, remote_path, verbose, readme) =
{name = name, parent = parent, session = session, path = path, html_prefix = html_prefix,
- info = info, doc_format = doc_format, doc_graph = doc_graph, documents = documents,
- doc_dump = doc_dump, remote_path = remote_path, verbose = verbose,
- readme = readme}: session_info;
+ info = info, doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output,
+ documents = documents, doc_dump = doc_dump, remote_path = remote_path,
+ verbose = verbose, readme = readme}: session_info;
(* state *)
@@ -274,16 +275,12 @@
| [name, tags] => (name, tags)
| _ => error ("Malformed document variant specification: " ^ quote str));
-fun read_variants strs =
- rev (distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_variant strs)))
- |> filter_out (fn (_, s) => s = "-");
-
(* init session *)
fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
-fun init build info info_path doc doc_graph doc_variants path name
+fun init build info info_path doc doc_graph document_output doc_variants path name
(doc_dump as (dump_prefix, _)) (remote_path, first_time) verbose thys =
if not build andalso not info andalso doc = "" andalso dump_prefix = "" then
(browser_info := empty_browser_info; session_info := NONE)
@@ -293,13 +290,14 @@
val session_name = name_of_session path;
val sess_prefix = Path.make path;
val html_prefix = Path.append (Path.expand (Path.explode info_path)) sess_prefix;
+ val doc_output = if document_output = "" then NONE else SOME (Path.explode document_output);
val documents =
if doc = "" then []
else if not (can File.check_dir document_path) then
(if verbose then Output.physical_stderr "Warning: missing document directory\n"
else (); [])
- else read_variants doc_variants;
+ else doc_variants;
val parent_index_path = Path.append Path.parent index_path;
val index_up_lnk =
@@ -318,8 +316,8 @@
(Url.File index_path, session_name) docs (Url.explode "medium.html");
in
session_info :=
- SOME (make_session_info (name, parent_name, session_name, path, html_prefix,
- info, doc, doc_graph, documents, doc_dump, remote_path, verbose, readme));
+ SOME (make_session_info (name, parent_name, session_name, path, html_prefix, info, doc,
+ doc_graph, doc_output, documents, doc_dump, remote_path, verbose, readme));
browser_info := init_browser_info remote_path path thys;
add_html_index (0, index_text)
end;
@@ -327,11 +325,11 @@
(* isabelle tool wrappers *)
-fun isabelle_document verbose format name tags path result_path =
+fun isabelle_document {verbose, purge} format name tags dir =
let
- val s = "\"$ISABELLE_TOOL\" document -c -o '" ^ format ^ "' \
- \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path path ^ " 2>&1";
- val doc_path = Path.append result_path (Path.ext format (Path.basic name));
+ val s = "\"$ISABELLE_TOOL\" document" ^ (if purge then " -c" else "") ^ " -o '" ^ format ^ "' \
+ \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path dir ^ " 2>&1";
+ val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format];
val _ = if verbose then writeln s else ();
val (out, rc) = Isabelle_System.bash_output s;
val _ =
@@ -369,8 +367,8 @@
fun finish () =
- session_default () (fn {name, info, html_prefix, doc_format,
- doc_graph, documents, doc_dump = (dump_prefix, dump_mode), path, verbose, readme, ...} =>
+ session_default () (fn {name, info, html_prefix, doc_format, doc_graph, doc_output,
+ documents, doc_dump = (dump_prefix, dump_mode), path, verbose, readme, ...} =>
let
val {theories, files, tex_index, html_index, graph} = ! browser_info;
val thys = Symtab.dest theories;
@@ -433,11 +431,19 @@
val doc_paths =
documents |> Par_List.map (fn (name, tags) =>
let
- val path = Path.append html_prefix (Path.basic name);
- val _ = prepare_sources path Dump_all;
- in isabelle_document true doc_format name tags path html_prefix end);
+ val (doc_prefix, purge) =
+ (case doc_output of
+ SOME path => (path, false)
+ | NONE => (html_prefix, true));
+ val _ =
+ File.eq (document_path, doc_prefix) andalso
+ error ("Overlap of document input and output directory " ^ Path.print doc_prefix);
+ val dir = Path.append doc_prefix (Path.basic name);
+ val mode = if File.eq (document_path, dir) then Dump_tex_sty else Dump_all;
+ val _ = prepare_sources dir mode;
+ in isabelle_document {verbose = true, purge = purge} doc_format name tags dir end);
val _ =
- if verbose then
+ if verbose orelse is_some doc_output then
doc_paths
|> List.app (fn doc => Output.physical_stderr ("Document at " ^ show_path doc ^ "\n"))
else ();
@@ -543,7 +549,8 @@
|> File.write (Path.append doc_path (tex_path name)));
val _ = write_tex_index tex_index doc_path;
- val result = isabelle_document false doc_format documentN "" doc_path dir;
+ val result =
+ isabelle_document {verbose = false, purge = true} doc_format documentN "" doc_path;
val result' = Isabelle_System.create_tmp_path documentN doc_format;
val _ = File.copy result result';
in result' end);
--- a/src/Tools/jEdit/lib/Tools/jedit Tue Aug 14 16:09:45 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Tue Aug 14 16:18:15 2012 +0200
@@ -52,6 +52,7 @@
echo " -J OPTION add JVM runtime option"
echo " (default JEDIT_JAVA_OPTIONS=$JEDIT_JAVA_OPTIONS)"
echo " -b build only"
+ echo " -d DIR include session directory"
echo " -f fresh build"
echo " -j OPTION add jEdit runtime option"
echo " (default JEDIT_OPTIONS=$JEDIT_OPTIONS)"
@@ -82,13 +83,14 @@
BUILD_ONLY=false
BUILD_JARS="jars"
+JEDIT_SESSION_DIRS=""
JEDIT_LOGIC="$ISABELLE_LOGIC"
JEDIT_PRINT_MODE=""
function getoptions()
{
OPTIND=1
- while getopts "J:bdfj:l:m:" OPT
+ while getopts "J:bd:fj:l:m:" OPT
do
case "$OPT" in
J)
@@ -97,6 +99,13 @@
b)
BUILD_ONLY=true
;;
+ d)
+ if [ -z "$JEDIT_SESSION_DIRS" ]; then
+ JEDIT_SESSION_DIRS="$OPTARG"
+ else
+ JEDIT_SESSION_DIRS="$JEDIT_SESSION_DIRS:$OPTARG"
+ fi
+ ;;
f)
BUILD_JARS="jars_fresh"
;;
@@ -283,7 +292,7 @@
;;
esac
- export JEDIT_LOGIC JEDIT_PRINT_MODE
+ export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE
exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \
-jar "$(jvmpath "$JEDIT_HOME/dist/jedit.jar")" \
--- a/src/Tools/jEdit/src/plugin.scala Tue Aug 14 16:09:45 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Tue Aug 14 16:18:15 2012 +0200
@@ -300,6 +300,7 @@
def start_session()
{
+ val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
val logic = {
val logic = Property("logic")
@@ -307,7 +308,7 @@
else Isabelle.default_logic()
}
val name = Path.explode(logic).base.implode // FIXME more robust session name
- session.start(name, modes ::: List(logic))
+ session.start(dirs, name, modes ::: List(logic))
}