--- a/src/HOL/ROOT Wed Jun 07 17:11:45 2017 -0400
+++ b/src/HOL/ROOT Wed Jun 07 23:23:48 2017 +0200
@@ -968,6 +968,8 @@
session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
options [show_question_marks = false, spark_prv = false]
+ sessions
+ "HOL-SPARK-Examples"
theories
Example_Verification
VC_Principles
--- a/src/Pure/Tools/imports.scala Wed Jun 07 17:11:45 2017 -0400
+++ b/src/Pure/Tools/imports.scala Wed Jun 07 23:23:48 2017 +0200
@@ -94,7 +94,7 @@
if (operation_imports) {
progress.echo("\nPotential session imports:")
- selected.sorted.foreach(session_name =>
+ selected.flatMap(session_name =>
{
val info = full_sessions(session_name)
val session_resources = new Resources(deps(session_name))
@@ -110,10 +110,11 @@
if !declared_imports.contains(qualifier)
} yield qualifier).toSet
- if (extra_imports.nonEmpty) {
- progress.echo("session " + Token.quote_name(root_keywords, session_name) + ": " +
- extra_imports.toList.sorted.map(Token.quote_name(root_keywords, _)).mkString(" "))
- }
+ if (extra_imports.isEmpty) None
+ else Some((session_name, extra_imports.toList.sorted, declared_imports.size))
+ }).sortBy(_._3).foreach({ case (session_name, extra_imports, _) =>
+ progress.echo("session " + Token.quote_name(root_keywords, session_name) + ": " +
+ extra_imports.map(Token.quote_name(root_keywords, _)).mkString(" "))
})
}
@@ -136,15 +137,16 @@
val info = full_sessions(session_name)
val session_base = deps(session_name)
val session_resources = new Resources(session_base)
- val imports_resources = new Resources(session_base.get_imports)
+ val imports_base = session_base.get_imports
+ val imports_resources = new Resources(imports_base)
def standard_import(qualifier: String, dir: String, s: String): String =
{
val name = imports_resources.import_name(qualifier, dir, s)
val s1 =
- if (session_base.loaded_theory(name)) name.theory
+ if (imports_base.loaded_theory(name)) name.theory
else {
- imports_resources.session_base.known.get_file(Path.explode(name.node).file) match {
+ imports_base.known.get_file(Path.explode(name.node).file) match {
case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
name1.theory
case Some(name1) if Thy_Header.is_base_name(s) =>
@@ -166,6 +168,7 @@
val updates_theories =
for {
(_, name) <- session_base.known.theories_local.toList
+ if session_resources.theory_qualifier(name) == info.theory_qualifier
(_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
upd <- update_name(session_base.syntax.keywords, pos,
standard_import(session_resources.theory_qualifier(name), name.master_dir, _))
--- a/src/Tools/VSCode/extension/src/preview.ts Wed Jun 07 17:11:45 2017 -0400
+++ b/src/Tools/VSCode/extension/src/preview.ts Wed Jun 07 23:23:48 2017 +0200
@@ -80,7 +80,12 @@
if (preview_uri) {
preview_content.set(preview_uri.toString(), params.content)
content_provider.update(preview_uri)
- if (params.column != 0) {
+
+ const existing_document =
+ workspace.textDocuments.find(document =>
+ document.uri.scheme === preview_uri.scheme &&
+ document.uri.query === preview_uri.query)
+ if (!existing_document && params.column != 0) {
commands.executeCommand("vscode.previewHtml", preview_uri, params.column, params.label)
}
}
--- a/src/Tools/jEdit/src/theories_dockable.scala Wed Jun 07 17:11:45 2017 -0400
+++ b/src/Tools/jEdit/src/theories_dockable.scala Wed Jun 07 23:23:48 2017 +0200
@@ -44,8 +44,11 @@
}
case MouseMoved(_, point, _) =>
val index = peer.locationToIndex(point)
- if (index >= 0 && in_checkbox(peer.indexToLocation(index), point))
+ val index_location = peer.indexToLocation(index)
+ if (index >= 0 && in_checkbox(index_location, point))
tooltip = "Mark as required for continuous checking"
+ if (index >= 0 && in_label(index_location, point))
+ tooltip = "theory " + quote(listData(index).theory)
else
tooltip = null
}
@@ -91,14 +94,20 @@
private var nodes_status: Map[Document.Node.Name, Protocol.Node_Status] = Map.empty
private var nodes_required: Set[Document.Node.Name] = Document_Model.required_nodes()
+ private def in(geometry: Option[(Point, Dimension)], loc0: Point, p: Point): Boolean =
+ geometry match {
+ case Some((loc, size)) =>
+ loc0.x + loc.x <= p.x && p.x < loc0.x + size.width &&
+ loc0.y + loc.y <= p.y && p.y < loc0.y + size.height
+ case None => false
+ }
+
private def in_checkbox(loc0: Point, p: Point): Boolean =
- Node_Renderer_Component != null &&
- (Node_Renderer_Component.checkbox_geometry match {
- case Some((loc, size)) =>
- loc0.x + loc.x <= p.x && p.x < loc0.x + size.width &&
- loc0.y + loc.y <= p.y && p.y < loc0.y + size.height
- case None => false
- })
+ Node_Renderer_Component != null && in(Node_Renderer_Component.checkbox_geometry, loc0, p)
+
+ private def in_label(loc0: Point, p: Point): Boolean =
+ Node_Renderer_Component != null && in(Node_Renderer_Component.label_geometry, loc0, p)
+
private object Node_Renderer_Component extends BorderPanel
{
@@ -118,6 +127,7 @@
}
}
+ var label_geometry: Option[(Point, Dimension)] = None
val label = new Label {
background = view.getTextArea.getPainter.getBackground
foreground = view.getTextArea.getPainter.getForeground
@@ -157,6 +167,9 @@
paint_segment(0, size.width, PIDE.options.color_value("unprocessed1_color"))
}
super.paintComponent(gfx)
+
+ if (location != null && size != null)
+ label_geometry = Some((location, size))
}
}