clarified signature -- eliminated somewhat pointless positions;
authorwenzelm
Fri Mar 23 22:53:32 2018 +0100 (14 months ago)
changeset 67940b4e80f062fbf
parent 67939 544a7a21298e
child 67941 49a34b2fa788
clarified signature -- eliminated somewhat pointless positions;
src/Doc/System/Server.thy
src/Pure/Thy/thy_resources.scala
src/Pure/Tools/server_commands.scala
     1.1 --- a/src/Doc/System/Server.thy	Fri Mar 23 22:44:43 2018 +0100
     1.2 +++ b/src/Doc/System/Server.thy	Fri Mar 23 22:53:32 2018 +0100
     1.3 @@ -877,13 +877,9 @@
     1.4    \end{tabular}
     1.5  
     1.6    \begin{tabular}{ll}
     1.7 -  \<^bold>\<open>type\<close> \<open>theory_name = string | {name: string, pos: position}\<close> \\
     1.8 -  \end{tabular}
     1.9 -
    1.10 -  \begin{tabular}{ll}
    1.11    \<^bold>\<open>type\<close> \<open>use_theories_arguments =\<close> \\
    1.12    \quad\<open>{session_id: uuid,\<close> \\
    1.13 -  \quad~~\<open>theories: [theory_name],\<close> \\
    1.14 +  \quad~~\<open>theories: [string],\<close> \\
    1.15    \quad~~\<open>master_dir?: string,\<close> \\
    1.16    \quad~~\<open>pretty_margin?: double\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>76\<close> \\
    1.17    \quad~~\<open>unicode_symbols?: bool}\<close> \\[2ex]
    1.18 @@ -925,9 +921,7 @@
    1.19  
    1.20    \<^medskip>
    1.21    The \<open>theories\<close> field specifies theory names as in theory \<^theory_text>\<open>imports\<close> or in
    1.22 -  ROOT \<^bold>\<open>theories\<close>. An explicit source position for these theory name
    1.23 -  specifications may be given, which is occasionally useful for precise error
    1.24 -  locations.
    1.25 +  ROOT \<^bold>\<open>theories\<close>.
    1.26  
    1.27    \<^medskip> The \<open>master_dir\<close> field specifies the master directory of imported
    1.28    theories: it acts like the ``current working directory'' for locating theory
     2.1 --- a/src/Pure/Thy/thy_resources.scala	Fri Mar 23 22:44:43 2018 +0100
     2.2 +++ b/src/Pure/Thy/thy_resources.scala	Fri Mar 23 22:53:32 2018 +0100
     2.3 @@ -90,7 +90,7 @@
     2.4      /* theories */
     2.5  
     2.6      def use_theories(
     2.7 -      theories: List[(String, Position.T)],
     2.8 +      theories: List[String],
     2.9        qualifier: String = Sessions.DRAFT,
    2.10        master_dir: String = "",
    2.11        id: UUID = UUID(),
    2.12 @@ -231,15 +231,12 @@
    2.13    def load_theories(
    2.14      session: Session,
    2.15      id: UUID,
    2.16 -    theories: List[(String, Position.T)],
    2.17 +    theories: List[String],
    2.18      qualifier: String = Sessions.DRAFT,
    2.19      master_dir: String = "",
    2.20      progress: Progress = No_Progress): List[Document.Node.Name] =
    2.21    {
    2.22 -    val import_names =
    2.23 -      for ((thy, pos) <- theories)
    2.24 -      yield (import_name(qualifier, master_dir, thy), pos)
    2.25 -
    2.26 +    val import_names = theories.map(thy => import_name(qualifier, master_dir, thy) -> Position.none)
    2.27      val dependencies = resources.dependencies(import_names, progress = progress).check_errors
    2.28      val dep_theories = dependencies.theories
    2.29  
     3.1 --- a/src/Pure/Tools/server_commands.scala	Fri Mar 23 22:44:43 2018 +0100
     3.2 +++ b/src/Pure/Tools/server_commands.scala	Fri Mar 23 22:53:32 2018 +0100
     3.3 @@ -11,17 +11,6 @@
     3.4  {
     3.5    def default_preferences: String = Options.read_prefs()
     3.6  
     3.7 -  def unapply_name_pos(json: JSON.T): Option[(String, Position.T)] =
     3.8 -    json match {
     3.9 -      case JSON.Value.String(name) => Some((name, Position.none))
    3.10 -      case JSON.Object(map) if map.keySet == Set("name", "pos") =>
    3.11 -      (map("name"), map("pos")) match {
    3.12 -        case (JSON.Value.String(name), Position.JSON(pos)) => Some((name, pos))
    3.13 -        case _ => None
    3.14 -      }
    3.15 -      case _ => None
    3.16 -    }
    3.17 -
    3.18    object Cancel
    3.19    {
    3.20      sealed case class Args(task: UUID)
    3.21 @@ -164,7 +153,7 @@
    3.22    {
    3.23      sealed case class Args(
    3.24        session_id: UUID,
    3.25 -      theories: List[(String, Position.T)],
    3.26 +      theories: List[String],
    3.27        master_dir: String = "",
    3.28        pretty_margin: Double = Pretty.default_margin,
    3.29        unicode_symbols: Boolean = false)
    3.30 @@ -172,7 +161,7 @@
    3.31      def unapply(json: JSON.T): Option[Args] =
    3.32        for {
    3.33          session_id <- JSON.uuid(json, "session_id")
    3.34 -        theories <- JSON.list(json, "theories", unapply_name_pos _)
    3.35 +        theories <- JSON.list(json, "theories", JSON.Value.String.unapply _)
    3.36          master_dir <- JSON.string_default(json, "master_dir")
    3.37          pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin)
    3.38          unicode_symbols <- JSON.bool_default(json, "unicode_symbols")