# HG changeset patch # User wenzelm # Date 1504203595 -7200 # Node ID 6a034c6c423fa2553d57d413d8f069eee2a0e8fe # Parent 52b5cf533fd6b92be518a422f5e52b8eaa30f41d# Parent 6e35cf3ce869173409be6b07f0fe218d6d22a259 merged diff -r 52b5cf533fd6 -r 6a034c6c423f NEWS --- 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 diff -r 52b5cf533fd6 -r 6a034c6c423f src/Doc/JEdit/JEdit.thy --- 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>\-n\ option bypasses the implicit build process for the selected session image. - Option \<^verbatim>\-R\ modifies the meaning of option \<^verbatim>\-l\~\session\ as follows: the - parent image of the \session\ is used, with qualified theory imports - restricted to that portion of the session graph. Moreover, the \<^verbatim>\ROOT\ entry - of the \session\ is opened in the editor. This facilitates maintenance of a - particular session, by moving the Prover IDE quickly to relevant source - files. + Option \<^verbatim>\-R\ modifies the meaning of option \<^verbatim>\-l\ as follows: the \<^verbatim>\ROOT\ + 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>\-m\ option specifies additional print modes for the prover process. Note that the system option @{system_option_ref jedit_print_mode} allows to diff -r 52b5cf533fd6 -r 6a034c6c423f src/Doc/System/Sessions.thy --- 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>\ROOTS\ line-by-line. This helps to organize large collections of session specifications, or to make - \<^verbatim>\-d\ command line options persistent (say within + \<^verbatim>\-d\ command line options persistent (e.g.\ in \<^verbatim>\$ISABELLE_HOME_USER/ROOTS\). \<^medskip> diff -r 52b5cf533fd6 -r 6a034c6c423f src/Pure/Admin/build_history.scala --- 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 */ diff -r 52b5cf533fd6 -r 6a034c6c423f src/Pure/General/mercurial.scala --- 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] diff -r 52b5cf533fd6 -r 6a034c6c423f src/Pure/General/ssh.scala --- 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 } diff -r 52b5cf533fd6 -r 6a034c6c423f src/Pure/Thy/sessions.scala --- 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)) } diff -r 52b5cf533fd6 -r 6a034c6c423f src/Pure/Tools/build.scala --- 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 diff -r 52b5cf533fd6 -r 6a034c6c423f src/Pure/Tools/imports.scala --- 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 diff -r 52b5cf533fd6 -r 6a034c6c423f src/Pure/Tools/main.scala --- 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") diff -r 52b5cf533fd6 -r 6a034c6c423f src/Tools/jEdit/lib/Tools/jedit --- 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[@]}" diff -r 52b5cf533fd6 -r 6a034c6c423f src/Tools/jEdit/src/jedit_resources.scala --- 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 */ diff -r 52b5cf533fd6 -r 6a034c6c423f src/Tools/jEdit/src/jedit_sessions.scala --- 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") diff -r 52b5cf533fd6 -r 6a034c6c423f src/Tools/jEdit/src/plugin.scala --- 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)