clarified theory node name;
authorwenzelm
Sat Mar 24 20:45:30 2018 +0100 (16 months ago)
changeset 67943b45f0c0ea14f
parent 67942 a3e5f08e6b58
child 67944 cb2b1a75ff59
clarified theory node name;
purge_theories: return purged, retained;
tuned documentation;
src/Doc/System/Server.thy
src/Pure/PIDE/document.scala
src/Pure/Thy/thy_resources.scala
src/Pure/Tools/server_commands.scala
     1.1 --- a/src/Doc/System/Server.thy	Sat Mar 24 15:07:13 2018 +0100
     1.2 +++ b/src/Doc/System/Server.thy	Sat Mar 24 20:45:30 2018 +0100
     1.3 @@ -509,6 +509,12 @@
     1.4    connections and may be shared by different clients, as long as the internal
     1.5    session identifier is known.
     1.6  
     1.7 +  \<^item> \<^bold>\<open>type\<close> \<open>node = {node_name: string, theory_name: string}\<close> represents the
     1.8 +  internal node name of a theory. The \<open>node_name\<close> is derived from the
     1.9 +  canonical theory file-name (e.g.\ \<^verbatim>\<open>"~~/src/HOL/ex/Seq.thy"\<close> after
    1.10 +  normalization within the file-system). The \<open>theory_name\<close> is the
    1.11 +  session-qualified theory name (e.g.\ \<^verbatim>\<open>HOL-ex.Seq\<close>).
    1.12 +
    1.13    \<^item> \<^bold>\<open>type\<close> \<open>node_status = {ok: bool, total: int, unprocessed: int, running:
    1.14    int, warned: int, failed: int, finished: int, consolidated: bool}\<close>
    1.15    represents a formal theory node status of the PIDE document model. Fields
    1.16 @@ -888,15 +894,13 @@
    1.17  
    1.18    \begin{tabular}{ll}
    1.19    \<^bold>\<open>type\<close> \<open>node_result =\<close> \\
    1.20 -  \quad\<open>{node_name: string,\<close> \\
    1.21 -  \quad~~\<open>theory: string,\<close> \\
    1.22 -  \quad~~\<open>status: node_status,\<close> \\
    1.23 +  \quad\<open>{status: node_status,\<close> \\
    1.24    \quad~~\<open>messages: [message]}\<close> \\[2ex]
    1.25  
    1.26    \<^bold>\<open>type\<close> \<open>use_theories_results =\<close> \\
    1.27    \quad\<open>{ok: bool,\<close> \\
    1.28    \quad~~\<open>errors: [message],\<close> \\
    1.29 -  \quad~~\<open>nodes: [node_result]}\<close> \\[2ex]
    1.30 +  \quad~~\<open>nodes: [node \<oplus> node_result]}\<close> \\[2ex]
    1.31    \end{tabular}
    1.32  
    1.33    \<^medskip>
    1.34 @@ -928,9 +932,9 @@
    1.35    \<^medskip>
    1.36    The \<open>master_dir\<close> field specifies the master directory of imported theories:
    1.37    it acts like the ``current working directory'' for locating theory files.
    1.38 -  This may be omitted if all entries of \<open>theories\<close> use a session-qualified
    1.39 -  theory name (e.g.\ \<^verbatim>\<open>"HOL-Library.AList"\<close>) or absolute path name (e.g.\
    1.40 -  \<^verbatim>\<open>"~~/src/HOL/ex/Seq"\<close>).
    1.41 +  This may be omitted if all entries of \<open>theories\<close> use an absolute path name
    1.42 +  (e.g.\ \<^verbatim>\<open>"~~/src/HOL/ex/Seq.thy"\<close>) or session-qualified theory name (e.g.\
    1.43 +  \<^verbatim>\<open>"HOL-ex/Seq"\<close>).
    1.44  
    1.45    \<^medskip>
    1.46    The \<open>pretty_margin\<close> field specifies the line width for pretty-printing. The
    1.47 @@ -961,10 +965,10 @@
    1.48    The \<open>nodes\<close> field provides detailed information about each imported theory
    1.49    node. The individual fields are as follows:
    1.50  
    1.51 -  \<^item> \<open>node_name\<close>: the physical name for the theory node, based on its
    1.52 +  \<^item> \<open>node_name\<close>: the canonical name for the theory node, based on its
    1.53    file-system location;
    1.54  
    1.55 -  \<^item> \<open>theory\<close>: the logical theory name, e.g.\ \<^verbatim>\<open>HOL-Library.AList\<close>;
    1.56 +  \<^item> \<open>theory_name\<close>: the logical theory name;
    1.57  
    1.58    \<^item> \<open>status\<close>: the overall node status, e.g.\ see the visualization in the
    1.59    \<open>Theories\<close> panel of Isabelle/jEdit @{cite "isabelle-jedit"};
    1.60 @@ -1040,8 +1044,9 @@
    1.61    \<open>node_name\<close>.
    1.62  
    1.63    \<^medskip>
    1.64 -  The \<open>master_dir\<close> field specifies the master directory as in \<^verbatim>\<open>use_theories\<close>;
    1.65 -  by passing its \<open>nodes\<close> / \<open>node_name\<close> results, the \<open>master_dir\<close> is redundant.
    1.66 +  The \<open>master_dir\<close> field specifies the master directory as in \<^verbatim>\<open>use_theories\<close>.
    1.67 +  It is redundant, when passing fully-qualified theory node names (e.g.\
    1.68 +  \<open>node_name\<close> from \<open>nodes\<close> in \<open>use_theories_results\<close>).
    1.69  
    1.70    \<^medskip>
    1.71    The \<open>all\<close> field set to \<^verbatim>\<open>true\<close> attempts to purge all presently loaded
    1.72 @@ -1052,8 +1057,11 @@
    1.73  subsubsection \<open>Results\<close>
    1.74  
    1.75  text \<open>
    1.76 -  The \<open>purged\<close> field reveals the \<open>node_name\<close> of each theory that was actually
    1.77 -  removed.
    1.78 +  The \<open>purged\<close> field gives the theory nodes that were actually removed.
    1.79 +
    1.80 +  \<^medskip>
    1.81 +  The \<open>retained\<close> field gives the remaining theory nodes, i.e.\ the complement
    1.82 +  of \<open>purged\<close>.
    1.83  \<close>
    1.84  
    1.85  end
     2.1 --- a/src/Pure/PIDE/document.scala	Sat Mar 24 15:07:13 2018 +0100
     2.2 +++ b/src/Pure/PIDE/document.scala	Sat Mar 24 20:45:30 2018 +0100
     2.3 @@ -130,6 +130,9 @@
     2.4  
     2.5        def map(f: String => String): Name = copy(f(node), f(master_dir), theory)
     2.6        def map_theory(f: String => String): Name = copy(node, master_dir, f(theory))
     2.7 +
     2.8 +      def json: JSON.Object.T =
     2.9 +        JSON.Object("node_name" -> node, "theory_name" -> theory)
    2.10      }
    2.11  
    2.12      sealed case class Entry(name: Node.Name, header: Node.Header)
     3.1 --- a/src/Pure/Thy/thy_resources.scala	Sat Mar 24 15:07:13 2018 +0100
     3.2 +++ b/src/Pure/Thy/thy_resources.scala	Sat Mar 24 20:45:30 2018 +0100
     3.3 @@ -142,7 +142,7 @@
     3.4          theories: List[String],
     3.5          qualifier: String = Sessions.DRAFT,
     3.6          master_dir: String = "",
     3.7 -        all: Boolean = false): List[Document.Node.Name] =
     3.8 +        all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) =
     3.9        resources.purge_theories(session, theories = theories, qualifier = qualifier,
    3.10          master_dir = master_dir, all = all)
    3.11    }
    3.12 @@ -294,7 +294,7 @@
    3.13      theories: List[String],
    3.14      qualifier: String = Sessions.DRAFT,
    3.15      master_dir: String = "",
    3.16 -    all: Boolean = false): List[Document.Node.Name] =
    3.17 +    all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) =
    3.18    {
    3.19      val nodes = theories.map(import_name(qualifier, master_dir, _))
    3.20  
    3.21 @@ -306,12 +306,14 @@
    3.22          val purge =
    3.23            (if (all) all_nodes else nodes.filter(graph.defined(_))).
    3.24              filterNot(st.is_required(_)).toSet
    3.25 -        val purged = all_nodes.filterNot(graph.all_preds(all_nodes.filterNot(purge)).toSet)
    3.26 +
    3.27 +        val retain = graph.all_preds(all_nodes.filterNot(purge)).toSet
    3.28 +        val (retained, purged) = all_nodes.partition(retain)
    3.29  
    3.30          val purge_edits = purged.flatMap(name => st.theories(name).purge_edits)
    3.31          session.update(Document.Blobs.empty, purge_edits)
    3.32  
    3.33 -        (purged, st.remove_theories(purged))
    3.34 +        ((purged, retained), st.remove_theories(purged))
    3.35        })
    3.36    }
    3.37  }
     4.1 --- a/src/Pure/Tools/server_commands.scala	Sat Mar 24 15:07:13 2018 +0100
     4.2 +++ b/src/Pure/Tools/server_commands.scala	Sat Mar 24 20:45:30 2018 +0100
     4.3 @@ -208,11 +208,9 @@
     4.4              } yield output_message(tree, pos)),
     4.5            "nodes" ->
     4.6              (for ((name, status) <- result.nodes) yield
     4.7 -              JSON.Object(
     4.8 -                "node_name" -> name.node,
     4.9 -                "theory" -> name.theory,
    4.10 -                "status" -> status.json,
    4.11 -                "messages" ->
    4.12 +              name.json +
    4.13 +                ("status" -> status.json) +
    4.14 +                ("messages" ->
    4.15                    (for ((tree, pos) <- result.messages(name))
    4.16                      yield output_message(tree, pos)))))
    4.17  
    4.18 @@ -238,12 +236,16 @@
    4.19        yield { Args(session_id, theories = theories, master_dir = master_dir, all = all) }
    4.20  
    4.21      def command(args: Args, session: Thy_Resources.Session)
    4.22 -      : (JSON.Object.T, List[Document.Node.Name]) =
    4.23 +      : (JSON.Object.T, (List[Document.Node.Name], List[Document.Node.Name])) =
    4.24      {
    4.25 -      val purged =
    4.26 +      val (purged, retained) =
    4.27          session.purge_theories(
    4.28            theories = args.theories, master_dir = args.master_dir, all = args.all)
    4.29 -      (JSON.Object("purged" -> purged.map(_.node)), purged)
    4.30 +
    4.31 +      val result_json =
    4.32 +        JSON.Object("purged" -> purged.map(_.json), "retained" -> retained.map(_.json))
    4.33 +
    4.34 +      (result_json, (purged, retained))
    4.35      }
    4.36    }
    4.37  }