# HG changeset patch
# User wenzelm
# Date 1496870628 -7200
# Node ID ded1c636aecec7e60d6c9cc5cabf0069ca11dcb1
# Parent  704e4970d7034fb706edea985421c2561ec6a339# Parent  e4a8e1e20d45b2ff2aff5d0cbdb625292b72e358
merged

diff -r 704e4970d703 -r ded1c636aece src/HOL/ROOT
--- 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
diff -r 704e4970d703 -r ded1c636aece src/Pure/Tools/imports.scala
--- 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, _))
diff -r 704e4970d703 -r ded1c636aece src/Tools/VSCode/extension/src/preview.ts
--- 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)
         }
       }
diff -r 704e4970d703 -r ded1c636aece src/Tools/jEdit/src/theories_dockable.scala
--- 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))
       }
     }