# HG changeset patch
# User wenzelm
# Date 1521842012 -3600
# Node ID b4e80f062fbfbc6deef66d269ee67ac2f8d3ca1c
# Parent  544a7a21298ec7cc3dc7b0a665300f227c2be0f0
clarified signature -- eliminated somewhat pointless positions;

diff -r 544a7a21298e -r b4e80f062fbf src/Doc/System/Server.thy
--- a/src/Doc/System/Server.thy	Fri Mar 23 22:44:43 2018 +0100
+++ b/src/Doc/System/Server.thy	Fri Mar 23 22:53:32 2018 +0100
@@ -877,13 +877,9 @@
   \end{tabular}
 
   \begin{tabular}{ll}
-  \<^bold>\<open>type\<close> \<open>theory_name = string | {name: string, pos: position}\<close> \\
-  \end{tabular}
-
-  \begin{tabular}{ll}
   \<^bold>\<open>type\<close> \<open>use_theories_arguments =\<close> \\
   \quad\<open>{session_id: uuid,\<close> \\
-  \quad~~\<open>theories: [theory_name],\<close> \\
+  \quad~~\<open>theories: [string],\<close> \\
   \quad~~\<open>master_dir?: string,\<close> \\
   \quad~~\<open>pretty_margin?: double\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>76\<close> \\
   \quad~~\<open>unicode_symbols?: bool}\<close> \\[2ex]
@@ -925,9 +921,7 @@
 
   \<^medskip>
   The \<open>theories\<close> field specifies theory names as in theory \<^theory_text>\<open>imports\<close> or in
-  ROOT \<^bold>\<open>theories\<close>. An explicit source position for these theory name
-  specifications may be given, which is occasionally useful for precise error
-  locations.
+  ROOT \<^bold>\<open>theories\<close>.
 
   \<^medskip> The \<open>master_dir\<close> field specifies the master directory of imported
   theories: it acts like the ``current working directory'' for locating theory
diff -r 544a7a21298e -r b4e80f062fbf src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Fri Mar 23 22:44:43 2018 +0100
+++ b/src/Pure/Thy/thy_resources.scala	Fri Mar 23 22:53:32 2018 +0100
@@ -90,7 +90,7 @@
     /* theories */
 
     def use_theories(
-      theories: List[(String, Position.T)],
+      theories: List[String],
       qualifier: String = Sessions.DRAFT,
       master_dir: String = "",
       id: UUID = UUID(),
@@ -231,15 +231,12 @@
   def load_theories(
     session: Session,
     id: UUID,
-    theories: List[(String, Position.T)],
+    theories: List[String],
     qualifier: String = Sessions.DRAFT,
     master_dir: String = "",
     progress: Progress = No_Progress): List[Document.Node.Name] =
   {
-    val import_names =
-      for ((thy, pos) <- theories)
-      yield (import_name(qualifier, master_dir, thy), pos)
-
+    val import_names = theories.map(thy => import_name(qualifier, master_dir, thy) -> Position.none)
     val dependencies = resources.dependencies(import_names, progress = progress).check_errors
     val dep_theories = dependencies.theories
 
diff -r 544a7a21298e -r b4e80f062fbf src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Fri Mar 23 22:44:43 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala	Fri Mar 23 22:53:32 2018 +0100
@@ -11,17 +11,6 @@
 {
   def default_preferences: String = Options.read_prefs()
 
-  def unapply_name_pos(json: JSON.T): Option[(String, Position.T)] =
-    json match {
-      case JSON.Value.String(name) => Some((name, Position.none))
-      case JSON.Object(map) if map.keySet == Set("name", "pos") =>
-      (map("name"), map("pos")) match {
-        case (JSON.Value.String(name), Position.JSON(pos)) => Some((name, pos))
-        case _ => None
-      }
-      case _ => None
-    }
-
   object Cancel
   {
     sealed case class Args(task: UUID)
@@ -164,7 +153,7 @@
   {
     sealed case class Args(
       session_id: UUID,
-      theories: List[(String, Position.T)],
+      theories: List[String],
       master_dir: String = "",
       pretty_margin: Double = Pretty.default_margin,
       unicode_symbols: Boolean = false)
@@ -172,7 +161,7 @@
     def unapply(json: JSON.T): Option[Args] =
       for {
         session_id <- JSON.uuid(json, "session_id")
-        theories <- JSON.list(json, "theories", unapply_name_pos _)
+        theories <- JSON.list(json, "theories", JSON.Value.String.unapply _)
         master_dir <- JSON.string_default(json, "master_dir")
         pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin)
         unicode_symbols <- JSON.bool_default(json, "unicode_symbols")