merged
authorwenzelm
Wed Jun 07 23:23:48 2017 +0200 (23 months ago)
changeset 66034ded1c636aece
parent 66026 704e4970d703
parent 66033 e4a8e1e20d45
child 66035 de6cd60b1226
child 66036 b6396880b644
merged
     1.1 --- a/src/HOL/ROOT	Wed Jun 07 17:11:45 2017 -0400
     1.2 +++ b/src/HOL/ROOT	Wed Jun 07 23:23:48 2017 +0200
     1.3 @@ -968,6 +968,8 @@
     1.4  
     1.5  session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
     1.6    options [show_question_marks = false, spark_prv = false]
     1.7 +  sessions
     1.8 +    "HOL-SPARK-Examples"
     1.9    theories
    1.10      Example_Verification
    1.11      VC_Principles
     2.1 --- a/src/Pure/Tools/imports.scala	Wed Jun 07 17:11:45 2017 -0400
     2.2 +++ b/src/Pure/Tools/imports.scala	Wed Jun 07 23:23:48 2017 +0200
     2.3 @@ -94,7 +94,7 @@
     2.4  
     2.5      if (operation_imports) {
     2.6        progress.echo("\nPotential session imports:")
     2.7 -      selected.sorted.foreach(session_name =>
     2.8 +      selected.flatMap(session_name =>
     2.9        {
    2.10          val info = full_sessions(session_name)
    2.11          val session_resources = new Resources(deps(session_name))
    2.12 @@ -110,10 +110,11 @@
    2.13              if !declared_imports.contains(qualifier)
    2.14            } yield qualifier).toSet
    2.15  
    2.16 -        if (extra_imports.nonEmpty) {
    2.17 -          progress.echo("session " + Token.quote_name(root_keywords, session_name) + ": " +
    2.18 -            extra_imports.toList.sorted.map(Token.quote_name(root_keywords, _)).mkString(" "))
    2.19 -        }
    2.20 +        if (extra_imports.isEmpty) None
    2.21 +        else Some((session_name, extra_imports.toList.sorted, declared_imports.size))
    2.22 +      }).sortBy(_._3).foreach({ case (session_name, extra_imports, _) =>
    2.23 +        progress.echo("session " + Token.quote_name(root_keywords, session_name) + ": " +
    2.24 +          extra_imports.map(Token.quote_name(root_keywords, _)).mkString(" "))
    2.25        })
    2.26      }
    2.27  
    2.28 @@ -136,15 +137,16 @@
    2.29            val info = full_sessions(session_name)
    2.30            val session_base = deps(session_name)
    2.31            val session_resources = new Resources(session_base)
    2.32 -          val imports_resources = new Resources(session_base.get_imports)
    2.33 +          val imports_base = session_base.get_imports
    2.34 +          val imports_resources = new Resources(imports_base)
    2.35  
    2.36            def standard_import(qualifier: String, dir: String, s: String): String =
    2.37            {
    2.38              val name = imports_resources.import_name(qualifier, dir, s)
    2.39              val s1 =
    2.40 -              if (session_base.loaded_theory(name)) name.theory
    2.41 +              if (imports_base.loaded_theory(name)) name.theory
    2.42                else {
    2.43 -                imports_resources.session_base.known.get_file(Path.explode(name.node).file) match {
    2.44 +                imports_base.known.get_file(Path.explode(name.node).file) match {
    2.45                    case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
    2.46                      name1.theory
    2.47                    case Some(name1) if Thy_Header.is_base_name(s) =>
    2.48 @@ -166,6 +168,7 @@
    2.49            val updates_theories =
    2.50              for {
    2.51                (_, name) <- session_base.known.theories_local.toList
    2.52 +              if session_resources.theory_qualifier(name) == info.theory_qualifier
    2.53                (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
    2.54                upd <- update_name(session_base.syntax.keywords, pos,
    2.55                  standard_import(session_resources.theory_qualifier(name), name.master_dir, _))
     3.1 --- a/src/Tools/VSCode/extension/src/preview.ts	Wed Jun 07 17:11:45 2017 -0400
     3.2 +++ b/src/Tools/VSCode/extension/src/preview.ts	Wed Jun 07 23:23:48 2017 +0200
     3.3 @@ -80,7 +80,12 @@
     3.4        if (preview_uri) {
     3.5          preview_content.set(preview_uri.toString(), params.content)
     3.6          content_provider.update(preview_uri)
     3.7 -        if (params.column != 0) {
     3.8 +
     3.9 +        const existing_document =
    3.10 +          workspace.textDocuments.find(document =>
    3.11 +            document.uri.scheme === preview_uri.scheme &&
    3.12 +            document.uri.query === preview_uri.query)
    3.13 +        if (!existing_document && params.column != 0) {
    3.14            commands.executeCommand("vscode.previewHtml", preview_uri, params.column, params.label)
    3.15          }
    3.16        }
     4.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Jun 07 17:11:45 2017 -0400
     4.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Jun 07 23:23:48 2017 +0200
     4.3 @@ -44,8 +44,11 @@
     4.4          }
     4.5        case MouseMoved(_, point, _) =>
     4.6          val index = peer.locationToIndex(point)
     4.7 -        if (index >= 0 && in_checkbox(peer.indexToLocation(index), point))
     4.8 +        val index_location = peer.indexToLocation(index)
     4.9 +        if (index >= 0 && in_checkbox(index_location, point))
    4.10            tooltip = "Mark as required for continuous checking"
    4.11 +        if (index >= 0 && in_label(index_location, point))
    4.12 +          tooltip = "theory " + quote(listData(index).theory)
    4.13          else
    4.14            tooltip = null
    4.15      }
    4.16 @@ -91,14 +94,20 @@
    4.17    private var nodes_status: Map[Document.Node.Name, Protocol.Node_Status] = Map.empty
    4.18    private var nodes_required: Set[Document.Node.Name] = Document_Model.required_nodes()
    4.19  
    4.20 +  private def in(geometry: Option[(Point, Dimension)], loc0: Point, p: Point): Boolean =
    4.21 +    geometry match {
    4.22 +      case Some((loc, size)) =>
    4.23 +        loc0.x + loc.x <= p.x && p.x < loc0.x + size.width &&
    4.24 +        loc0.y + loc.y <= p.y && p.y < loc0.y + size.height
    4.25 +      case None => false
    4.26 +    }
    4.27 +
    4.28    private def in_checkbox(loc0: Point, p: Point): Boolean =
    4.29 -    Node_Renderer_Component != null &&
    4.30 -      (Node_Renderer_Component.checkbox_geometry match {
    4.31 -        case Some((loc, size)) =>
    4.32 -          loc0.x + loc.x <= p.x && p.x < loc0.x + size.width &&
    4.33 -          loc0.y + loc.y <= p.y && p.y < loc0.y + size.height
    4.34 -        case None => false
    4.35 -      })
    4.36 +    Node_Renderer_Component != null && in(Node_Renderer_Component.checkbox_geometry, loc0, p)
    4.37 +
    4.38 +  private def in_label(loc0: Point, p: Point): Boolean =
    4.39 +    Node_Renderer_Component != null && in(Node_Renderer_Component.label_geometry, loc0, p)
    4.40 +
    4.41  
    4.42    private object Node_Renderer_Component extends BorderPanel
    4.43    {
    4.44 @@ -118,6 +127,7 @@
    4.45        }
    4.46      }
    4.47  
    4.48 +    var label_geometry: Option[(Point, Dimension)] = None
    4.49      val label = new Label {
    4.50        background = view.getTextArea.getPainter.getBackground
    4.51        foreground = view.getTextArea.getPainter.getForeground
    4.52 @@ -157,6 +167,9 @@
    4.53              paint_segment(0, size.width, PIDE.options.color_value("unprocessed1_color"))
    4.54          }
    4.55          super.paintComponent(gfx)
    4.56 +
    4.57 +        if (location != null && size != null)
    4.58 +          label_geometry = Some((location, size))
    4.59        }
    4.60      }
    4.61