--- a/NEWS Thu Aug 31 17:48:20 2017 +0200
+++ b/NEWS Thu Aug 31 20:19:55 2017 +0200
@@ -100,10 +100,9 @@
* Action "isabelle.preview" opens an HTML preview of the current theory
document in the default web browser.
-* Command-line invocation "isabelle jedit -R -l SESSION" uses the parent
-image of the SESSION, with qualified theory imports restricted to that
-portion of the session graph. Moreover, the ROOT entry of the SESSION is
-opened in the editor.
+* Command-line invocation "isabelle jedit -R -l LOGIC" opens the ROOT
+entry of the specified logic session in the editor, while its parent is
+used for formal checking.
* The main Isabelle/jEdit plugin may be restarted manually (using the
jEdit Plugin Manager), as long as the "Isabelle Base" plugin remains
--- a/src/Doc/JEdit/JEdit.thy Thu Aug 31 17:48:20 2017 +0200
+++ b/src/Doc/JEdit/JEdit.thy Thu Aug 31 20:19:55 2017 +0200
@@ -232,7 +232,7 @@
Options are:
-D NAME=X set JVM system property
-J OPTION add JVM runtime option
- -R restrict to parent of logic session and open its ROOT
+ -R open ROOT entry of logic session and use its parent
-b build only
-d DIR include session directory
-f fresh build
@@ -256,12 +256,10 @@
The \<^verbatim>\<open>-n\<close> option bypasses the implicit build process for the selected
session image.
- Option \<^verbatim>\<open>-R\<close> modifies the meaning of option \<^verbatim>\<open>-l\<close>~\<open>session\<close> as follows: the
- parent image of the \<open>session\<close> is used, with qualified theory imports
- restricted to that portion of the session graph. Moreover, the \<^verbatim>\<open>ROOT\<close> entry
- of the \<open>session\<close> is opened in the editor. This facilitates maintenance of a
- particular session, by moving the Prover IDE quickly to relevant source
- files.
+ Option \<^verbatim>\<open>-R\<close> modifies the meaning of option \<^verbatim>\<open>-l\<close> as follows: the \<^verbatim>\<open>ROOT\<close>
+ entry of the specified session is opened in the editor, while its parent
+ session is used for formal checking. This facilitates maintenance of a
+ broken session, by moving the Prover IDE quickly to relevant source files.
The \<^verbatim>\<open>-m\<close> option specifies additional print modes for the prover process.
Note that the system option @{system_option_ref jedit_print_mode} allows to
--- a/src/Doc/System/Sessions.thy Thu Aug 31 17:48:20 2017 +0200
+++ b/src/Doc/System/Sessions.thy Thu Aug 31 20:19:55 2017 +0200
@@ -318,7 +318,7 @@
Any session root directory may refer recursively to further directories of
the same kind, by listing them in a catalog file \<^verbatim>\<open>ROOTS\<close> line-by-line. This
helps to organize large collections of session specifications, or to make
- \<^verbatim>\<open>-d\<close> command line options persistent (say within
+ \<^verbatim>\<open>-d\<close> command line options persistent (e.g.\ in
\<^verbatim>\<open>$ISABELLE_HOME_USER/ROOTS\<close>).
\<^medskip>
--- a/src/Pure/Admin/build_history.scala Thu Aug 31 17:48:20 2017 +0200
+++ b/src/Pure/Admin/build_history.scala Thu Aug 31 20:19:55 2017 +0200
@@ -439,7 +439,7 @@
/* prepare repository clones */
val isabelle_hg =
- Mercurial.setup_repository(isabelle_repos_source, isabelle_repos_self, ssh = Some(ssh))
+ Mercurial.setup_repository(isabelle_repos_source, isabelle_repos_self, ssh = ssh)
if (self_update) {
val self_rev =
@@ -460,12 +460,12 @@
ssh.execute(ssh.bash_path(isabelle_admin + Path.explode("build")) + " jars_fresh").check
}
- if (Mercurial.is_repository(isabelle_repos_other, ssh = Some(ssh))) {
+ if (Mercurial.is_repository(isabelle_repos_other, ssh = ssh)) {
ssh.rm_tree(isabelle_repos_other)
}
val other_hg =
Mercurial.clone_repository(
- ssh.bash_path(isabelle_repos_self), isabelle_repos_other, rev = rev, ssh = Some(ssh))
+ ssh.bash_path(isabelle_repos_self), isabelle_repos_other, rev = rev, ssh = ssh)
/* Admin/build_history */
--- a/src/Pure/General/mercurial.scala Thu Aug 31 17:48:20 2017 +0200
+++ b/src/Pure/General/mercurial.scala Thu Aug 31 20:19:55 2017 +0200
@@ -28,82 +28,51 @@
/* repository access */
- def is_repository(root: Path, ssh: Option[SSH.Session] = None): Boolean =
- {
- val root_hg = root + Path.explode(".hg")
- val root_hg_present =
- ssh match {
- case None => root_hg.is_dir
- case Some(ssh) => ssh.is_dir(root_hg)
- }
- root_hg_present && new Repository(root, ssh).command("root").ok
- }
+ def is_repository(root: Path, ssh: SSH.System = SSH.Local): Boolean =
+ ssh.is_dir(root + Path.explode(".hg")) &&
+ new Repository(root, ssh).command("root").ok
- def repository(root: Path, ssh: Option[SSH.Session] = None): Repository =
+ def repository(root: Path, ssh: SSH.System = SSH.Local): Repository =
{
val hg = new Repository(root, ssh)
hg.command("root").check
hg
}
- def find_repository(start: Path, ssh: Option[SSH.Session] = None): Option[Repository] =
+ def find_repository(start: Path, ssh: SSH.System = SSH.Local): Option[Repository] =
{
def find(root: Path): Option[Repository] =
if (is_repository(root, ssh)) Some(repository(root, ssh = ssh))
else if (root.is_root) None
else find(root + Path.parent)
- ssh match {
- case None => find(start.expand)
- case Some(ssh) => find(ssh.expand_path(start))
- }
+ find(ssh.expand_path(start))
}
def clone_repository(source: String, root: Path, rev: String = "", options: String = "",
- ssh: Option[SSH.Session] = None): Repository =
+ ssh: SSH.System = SSH.Local): Repository =
{
val hg = new Repository(root, ssh)
- ssh match {
- case None => Isabelle_System.mkdirs(hg.root.dir)
- case Some(ssh) => ssh.mkdirs(hg.root.dir)
- }
+ ssh.mkdirs(hg.root.dir)
hg.command("clone", Bash.string(source) + " " + File.bash_path(hg.root) + opt_rev(rev), options)
.check
hg
}
- def setup_repository(source: String, root: Path, ssh: Option[SSH.Session] = None): Repository =
+ def setup_repository(source: String, root: Path, ssh: SSH.System = SSH.Local): Repository =
{
- val present =
- ssh match {
- case None => root.is_dir
- case Some(ssh) => ssh.is_dir(root)
- }
- if (present) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg }
+ if (ssh.is_dir(root)) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg }
else clone_repository(source, root, options = "--noupdate", ssh = ssh)
}
- class Repository private[Mercurial](root_path: Path, ssh: Option[SSH.Session])
+ class Repository private[Mercurial](root_path: Path, ssh: SSH.System = SSH.Local)
{
hg =>
- val root =
- ssh match {
- case None => root_path.expand
- case Some(ssh) => root_path.expand_env(ssh.settings)
- }
+ val root = ssh.expand_path(root_path)
+ def root_url: String = ssh.hg_url + root.implode
- def root_url: String =
- ssh match {
- case None => root.implode
- case Some(ssh) => ssh.hg_url + root.implode
- }
-
- override def toString: String =
- ssh match {
- case None => root.implode
- case Some(ssh) => ssh.toString + ":" + root.implode
- }
+ override def toString: String = ssh.prefix + root.implode
def command(name: String, args: String = "", options: String = ""): Process_Result =
{
@@ -111,10 +80,7 @@
"\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") +
(if (name == "clone") "" else " --repository " + File.bash_path(root)) +
" --noninteractive " + name + " " + options + " " + args
- ssh match {
- case None => Isabelle_System.bash(cmdline)
- case Some(ssh) => ssh.execute(cmdline)
- }
+ ssh.execute(cmdline)
}
def archive(target: String, rev: String = "", options: String = ""): Unit =
@@ -171,7 +137,7 @@
/* unknown files */
- def unknown_files(files: List[Path], ssh: Option[SSH.Session] = None): List[Path] =
+ def unknown_files(files: List[Path], ssh: SSH.System = SSH.Local): List[Path] =
{
val unknown = new mutable.ListBuffer[Path]
--- a/src/Pure/General/ssh.scala Thu Aug 31 17:48:20 2017 +0200
+++ b/src/Pure/General/ssh.scala Thu Aug 31 20:19:55 2017 +0200
@@ -255,14 +255,17 @@
/* session */
- class Session private[SSH](val options: Options, val session: JSch_Session)
+ class Session private[SSH](val options: Options, val session: JSch_Session) extends System
{
def update_options(new_options: Options): Session = new Session(new_options, session)
def user_prefix: String = if (session.getUserName == null) "" else session.getUserName + "@"
def host: String = if (session.getHost == null) "" else session.getHost
def port_suffix: String = if (session.getPort == default_port) "" else ":" + session.getPort
- def hg_url: String = "ssh://" + user_prefix + host + port_suffix + "/"
+ override def hg_url: String = "ssh://" + user_prefix + host + port_suffix + "/"
+
+ override def prefix: String =
+ user_prefix + host + port_suffix + ":"
override def toString: String =
user_prefix + host + port_suffix + (if (session.isConnected) "" else " (disconnected)")
@@ -289,7 +292,7 @@
val home = sftp.getHome
Map("HOME" -> home, "USER_HOME" -> home)
}
- def expand_path(path: Path): Path = path.expand_env(settings)
+ override def expand_path(path: Path): Path = path.expand_env(settings)
def remote_path(path: Path): String = expand_path(path).implode
def bash_path(path: Path): String = Bash.string(remote_path(path))
@@ -303,10 +306,10 @@
try { Some(Dir_Entry(expand_path(path), sftp.stat(remote_path(path)))) }
catch { case _: SftpException => None }
- def is_file(path: Path): Boolean = stat(path).map(_.is_file) getOrElse false
- def is_dir(path: Path): Boolean = stat(path).map(_.is_dir) getOrElse false
+ override def is_file(path: Path): Boolean = stat(path).map(_.is_file) getOrElse false
+ override def is_dir(path: Path): Boolean = stat(path).map(_.is_dir) getOrElse false
- def mkdirs(path: Path): Unit =
+ override def mkdirs(path: Path): Unit =
if (!is_dir(path)) {
execute(
"perl -e \"use File::Path make_path; make_path('" + remote_path(path) + "');\"")
@@ -363,7 +366,7 @@
new Exec(this, channel)
}
- def execute(command: String,
+ override def execute(command: String,
progress_stdout: String => Unit = (_: String) => (),
progress_stderr: String => Unit = (_: String) => (),
strict: Boolean = true): Process_Result =
@@ -386,4 +389,28 @@
try { body(Path.explode(remote_dir)) } finally { rm_tree(remote_dir) }
}
}
+
+
+
+ /* system operations */
+
+ trait System
+ {
+ def hg_url: String = ""
+ def prefix: String = ""
+
+ def expand_path(path: Path): Path = path.expand
+ def is_file(path: Path): Boolean = path.is_file
+ def is_dir(path: Path): Boolean = path.is_dir
+ def mkdirs(path: Path): Unit = Isabelle_System.mkdirs(path)
+
+ def execute(command: String,
+ progress_stdout: String => Unit = (_: String) => (),
+ progress_stderr: String => Unit = (_: String) => (),
+ strict: Boolean = true): Process_Result =
+ Isabelle_System.bash(command, progress_stdout = progress_stdout,
+ progress_stderr = progress_stderr, strict = strict)
+ }
+
+ object Local extends System
}
--- a/src/Pure/Thy/sessions.scala Thu Aug 31 17:48:20 2017 +0200
+++ b/src/Pure/Thy/sessions.scala Thu Aug 31 20:19:55 2017 +0200
@@ -100,6 +100,7 @@
}
sealed case class Base(
+ pos: Position.T = Position.none,
imports: Option[Base] = None,
global_theories: Map[String, String] = Map.empty,
loaded_theories: Map[String, String] = Map.empty,
@@ -107,7 +108,8 @@
keywords: Thy_Header.Keywords = Nil,
syntax: Outer_Syntax = Outer_Syntax.empty,
sources: List[(Path, SHA1.Digest)] = Nil,
- session_graph: Graph_Display.Graph = Graph_Display.empty_graph)
+ session_graph: Graph_Display.Graph = Graph_Display.empty_graph,
+ errors: List[String] = Nil)
{
def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
@@ -129,6 +131,20 @@
def is_empty: Boolean = session_bases.isEmpty
def apply(name: String): Base = session_bases(name)
def sources(name: String): List[SHA1.Digest] = session_bases(name).sources.map(_._2)
+
+ def errors: List[String] =
+ (for {
+ (name, base) <- session_bases.iterator
+ if base.errors.nonEmpty
+ } yield cat_lines(base.errors) +
+ "\nThe error(s) above occurred in session " + quote(name) + Position.here(base.pos)
+ ).toList
+
+ def check_errors: Deps =
+ errors match {
+ case Nil => this
+ case errs => error(cat_lines(errs))
+ }
}
def deps(sessions: T,
@@ -137,8 +153,7 @@
verbose: Boolean = false,
list_files: Boolean = false,
check_keywords: Set[String] = Set.empty,
- global_theories: Map[String, String] = Map.empty,
- all_known: Boolean = false): Deps =
+ global_theories: Map[String, String] = Map.empty): Deps =
{
val session_bases =
(Map.empty[String, Base] /: sessions.imports_topological_order)({
@@ -171,12 +186,7 @@
thys.map({ case (thy, pos) =>
(resources.import_name(info.theory_qualifier, info.dir.implode, thy), pos) })
})
- val thy_deps = resources.thy_info.dependencies(root_theories)
-
- thy_deps.errors match {
- case Nil => thy_deps
- case errs => error(cat_lines(errs))
- }
+ resources.thy_info.dependencies(root_theories)
}
val syntax = thy_deps.syntax
@@ -242,14 +252,17 @@
}
val base =
- Base(imports = Some(imports_base),
+ Base(
+ pos = info.pos,
+ imports = Some(imports_base),
global_theories = global_theories,
loaded_theories = thy_deps.loaded_theories,
known = Known.make(info.dir, List(imports_base), thy_deps.deps.map(_.name)),
keywords = thy_deps.keywords,
syntax = syntax,
sources = all_files.map(p => (p, SHA1.digest(p.file))),
- session_graph = session_graph)
+ session_graph = session_graph,
+ errors = thy_deps.errors)
session_bases + (info.name -> base)
}
@@ -260,9 +273,23 @@
}
})
- Deps(session_bases,
- if (all_known) Known.make(Path.current, session_bases.toList.map(_._2), Nil)
- else Known.empty)
+ Deps(session_bases, Known.make(Path.current, session_bases.toList.map(_._2), Nil))
+ }
+
+ def session_base_errors(
+ options: Options,
+ session: String,
+ dirs: List[Path] = Nil,
+ all_known: Boolean = false): (List[String], Base) =
+ {
+ val full_sessions = load(options, dirs = dirs)
+ val global_theories = full_sessions.global_theories
+ val (_, selected_sessions) = full_sessions.selection(Selection(sessions = List(session)))
+
+ val sessions: T = if (all_known) full_sessions else selected_sessions
+ val deps = Sessions.deps(sessions, global_theories = global_theories)
+ val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session)
+ (deps.errors, base)
}
def session_base(
@@ -271,17 +298,8 @@
dirs: List[Path] = Nil,
all_known: Boolean = false): Base =
{
- val full_sessions = load(options, dirs = dirs)
- val global_theories = full_sessions.global_theories
- val selected_sessions = full_sessions.selection(Selection(sessions = List(session)))._2
-
- if (all_known) {
- val deps =
- Sessions.deps(full_sessions, global_theories = global_theories, all_known = all_known)
- deps(session).copy(known = deps.all_known)
- }
- else
- deps(selected_sessions, global_theories = global_theories)(session)
+ val (errs, base) = session_base_errors(options, session, dirs = dirs, all_known = all_known)
+ if (errs.isEmpty) base else error(cat_lines(errs))
}
--- a/src/Pure/Tools/build.scala Thu Aug 31 17:48:20 2017 +0200
+++ b/src/Pure/Tools/build.scala Thu Aug 31 20:19:55 2017 +0200
@@ -377,7 +377,7 @@
val deps =
Sessions.deps(selected_sessions, progress = progress, inlined_files = true,
verbose = verbose, list_files = list_files, check_keywords = check_keywords,
- global_theories = full_sessions.global_theories)
+ global_theories = full_sessions.global_theories).check_errors
def sources_stamp(name: String): List[String] =
(selected_sessions(name).meta_digest :: deps.sources(name)).map(_.toString).sorted
--- a/src/Pure/Tools/imports.scala Thu Aug 31 17:48:20 2017 +0200
+++ b/src/Pure/Tools/imports.scala Thu Aug 31 20:19:55 2017 +0200
@@ -87,8 +87,7 @@
val deps =
Sessions.deps(selected_sessions, progress = progress, verbose = verbose,
- global_theories = full_sessions.global_theories,
- all_known = true)
+ global_theories = full_sessions.global_theories).check_errors
val root_keywords = Sessions.root_syntax.keywords
--- a/src/Pure/Tools/main.scala Thu Aug 31 17:48:20 2017 +0200
+++ b/src/Pure/Tools/main.scala Thu Aug 31 20:19:55 2017 +0200
@@ -23,6 +23,21 @@
GUI.install_fonts()
+ /* ROOTS template */
+
+ {
+ val roots = Path.explode("$ISABELLE_HOME_USER/ROOTS")
+ if (!roots.is_file) File.write(roots, """# Additional session root directories
+#
+# * each line contains one directory entry in Isabelle path notation
+# * lines starting with "#" are stripped
+# * changes require application restart
+#
+#:mode=text:encoding=UTF-8:
+""")
+ }
+
+
/* settings directory */
val settings_dir = Path.explode("$JEDIT_SETTINGS")
--- a/src/Tools/jEdit/lib/Tools/jedit Thu Aug 31 17:48:20 2017 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Thu Aug 31 20:19:55 2017 +0200
@@ -110,7 +110,7 @@
echo " Options are:"
echo " -D NAME=X set JVM system property"
echo " -J OPTION add JVM runtime option (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
- echo " -R restrict to parent of logic session and open its ROOT"
+ echo " -R open ROOT entry of logic session and use its parent"
echo " -b build only"
echo " -d DIR include session directory"
echo " -f fresh build"
@@ -148,7 +148,7 @@
BUILD_JARS="jars"
ML_PROCESS_POLICY=""
JEDIT_SESSION_DIRS=""
-JEDIT_LOGIC_RESTRICT=""
+JEDIT_LOGIC_ROOT=""
JEDIT_LOGIC=""
JEDIT_PRINT_MODE=""
JEDIT_BUILD_MODE="normal"
@@ -166,7 +166,7 @@
JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
;;
R)
- JEDIT_LOGIC_RESTRICT="true"
+ JEDIT_LOGIC_ROOT="true"
;;
b)
BUILD_ONLY=true
@@ -408,7 +408,7 @@
if [ "$BUILD_ONLY" = false ]
then
- export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_RESTRICT JEDIT_PRINT_MODE JEDIT_BUILD_MODE
+ export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ROOT JEDIT_PRINT_MODE JEDIT_BUILD_MODE
export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
classpath "$JEDIT_HOME/dist/jedit.jar"
exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
--- a/src/Tools/jEdit/src/jedit_resources.scala Thu Aug 31 17:48:20 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala Thu Aug 31 20:19:55 2017 +0200
@@ -21,7 +21,17 @@
import org.gjt.sp.jedit.bufferio.BufferIORequest
-class JEdit_Resources(session_base: Sessions.Base) extends Resources(session_base)
+object JEdit_Resources
+{
+ def apply(options: Options): JEdit_Resources =
+ {
+ val (errs, base) = JEdit_Sessions.session_base(options)
+ new JEdit_Resources(errs, base)
+ }
+}
+
+class JEdit_Resources private(val session_errors: List[String], session_base: Sessions.Base)
+ extends Resources(session_base)
{
/* document node name */
--- a/src/Tools/jEdit/src/jedit_sessions.scala Thu Aug 31 17:48:20 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Thu Aug 31 20:19:55 2017 +0200
@@ -30,9 +30,6 @@
case s => options.string("ML_process_policy") = s
}
- def session_restricted(): Boolean =
- Isabelle_System.getenv("JEDIT_LOGIC_RESTRICT") == "true"
-
def session_info(options: Options): Info =
{
val logic =
@@ -46,18 +43,18 @@
catch { case ERROR(_) => None }
info <- sessions.get(logic)
parent <- info.parent
- if session_restricted()
+ if Isabelle_System.getenv("JEDIT_LOGIC_ROOT") == "true"
} yield Info(parent, info.pos)) getOrElse Info(logic, Position.none)
}
def session_name(options: Options): String = session_info(options).name
- def session_base(options: Options): Sessions.Base =
+ def session_base(options: Options): (List[String], Sessions.Base) =
{
- val all_known = !session_restricted()
- Sessions.session_base(
- options, session_name(options), dirs = JEdit_Sessions.session_dirs(), all_known = all_known)
- .platform_path
+ val (errs, base) =
+ Sessions.session_base_errors(
+ options, session_name(options), dirs = JEdit_Sessions.session_dirs(), all_known = true)
+ (errs, base.platform_path)
}
def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
--- a/src/Tools/jEdit/src/plugin.scala Thu Aug 31 17:48:20 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Thu Aug 31 20:19:55 2017 +0200
@@ -70,8 +70,7 @@
/* resources */
private var _resources: JEdit_Resources = null
- private def init_resources(): Unit =
- _resources = new JEdit_Resources(JEdit_Sessions.session_base(options.value))
+ private def init_resources(): Unit = _resources = JEdit_Resources(options.value)
def resources: JEdit_Resources = _resources
@@ -311,6 +310,12 @@
"It is for testing only, not for production use.")
}
+ if (resources.session_errors.nonEmpty) {
+ GUI.warning_dialog(jEdit.getActiveView,
+ "Bad session structure: may cause problems with theory imports",
+ GUI.scrollable_text(cat_lines(resources.session_errors)))
+ }
+
val view = jEdit.getActiveView()
init_view(view)