# HG changeset patch # User wenzelm # Date 1344953895 -7200 # Node ID 559c1d80e129b1d90dde5991a902549222f4d771 # Parent ffa31bf5c662f9dcec07f370b0d3d9934fc739f0# Parent c3ea910b3581111b2e2c6ad52080e3d62dd55c9b merged diff -r ffa31bf5c662 -r 559c1d80e129 Admin/Release/makedist --- 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 <> $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 diff -r ffa31bf5c662 -r 559c1d80e129 NEWS --- 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 *** diff -r ffa31bf5c662 -r 559c1d80e129 doc-src/IsarRef/Thy/Inner_Syntax.thy --- 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 \} reads and prints types of the - meta-logic according to the current theory or proof context. + \item @{command "typ"}~@{text \} reads and prints a type expression + according to the current context. + + \item @{command "typ"}~@{text "\ :: s"} uses type-inference to + determine the most general way to make @{text "\"} conform to sort + @{text "s"}. For concrete @{text "\"} 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 \} read, type-check and print terms or propositions according to the diff -r ffa31bf5c662 -r 559c1d80e129 doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- 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 diff -r ffa31bf5c662 -r 559c1d80e129 doc-src/System/Thy/Interfaces.thy --- 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 diff -r ffa31bf5c662 -r 559c1d80e129 doc-src/System/Thy/Sessions.thy --- 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} *} diff -r ffa31bf5c662 -r 559c1d80e129 doc-src/System/Thy/document/Interfaces.tex --- 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 diff -r ffa31bf5c662 -r 559c1d80e129 doc-src/System/Thy/document/Sessions.tex --- 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% diff -r ffa31bf5c662 -r 559c1d80e129 etc/components --- 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 diff -r ffa31bf5c662 -r 559c1d80e129 etc/options --- 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)" diff -r ffa31bf5c662 -r 559c1d80e129 lib/Tools/mkroot --- 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" < 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)) ()); diff -r ffa31bf5c662 -r 559c1d80e129 src/Pure/Isar/isar_syn.ML --- 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" diff -r ffa31bf5c662 -r 559c1d80e129 src/Pure/PIDE/document.scala --- 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) diff -r ffa31bf5c662 -r 559c1d80e129 src/Pure/System/build.ML --- 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")) diff -r ffa31bf5c662 -r 559c1d80e129 src/Pure/System/build.scala --- 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 */ diff -r ffa31bf5c662 -r 559c1d80e129 src/Pure/System/options.scala --- 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) })) diff -r ffa31bf5c662 -r 559c1d80e129 src/Pure/System/session.ML --- 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 ())) diff -r ffa31bf5c662 -r 559c1d80e129 src/Pure/System/session.scala --- 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 } diff -r ffa31bf5c662 -r 559c1d80e129 src/Pure/Thy/present.ML --- 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); diff -r ffa31bf5c662 -r 559c1d80e129 src/Tools/jEdit/lib/Tools/jedit --- 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")" \ diff -r ffa31bf5c662 -r 559c1d80e129 src/Tools/jEdit/src/plugin.scala --- 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)) }