clarified modules and signature;
authorwenzelm
Thu Dec 13 15:21:34 2018 +0100 (19 months ago)
changeset 694585655af3ea5bd
parent 69457 bea49e443909
child 69459 bbb61a9cb99a
clarified modules and signature;
src/Pure/General/json.scala
src/Pure/General/uuid.scala
src/Pure/PIDE/headless.scala
src/Pure/ROOT.scala
src/Pure/Tools/server.scala
src/Pure/Tools/server_commands.scala
src/Pure/build-jars
src/Tools/VSCode/src/grammar.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/General/json.scala	Thu Dec 13 13:11:35 2018 +0100
     1.2 +++ b/src/Pure/General/json.scala	Thu Dec 13 15:21:34 2018 +0100
     1.3 @@ -244,11 +244,9 @@
     1.4    {
     1.5      object UUID
     1.6      {
     1.7 -      def unapply(json: T): Option[java.util.UUID] =
     1.8 +      def unapply(json: T): Option[isabelle.UUID.T] =
     1.9          json match {
    1.10 -          case x: java.lang.String =>
    1.11 -            try { Some(java.util.UUID.fromString(x)) }
    1.12 -            catch { case _: IllegalArgumentException => None }
    1.13 +          case x: java.lang.String => isabelle.UUID.unapply(x)
    1.14            case _ => None
    1.15          }
    1.16      }
    1.17 @@ -349,7 +347,7 @@
    1.18        case Some(json) => unapply(json)
    1.19      }
    1.20  
    1.21 -  def uuid(obj: T, name: String): Option[UUID] =
    1.22 +  def uuid(obj: T, name: String): Option[UUID.T] =
    1.23      value(obj, name, Value.UUID.unapply)
    1.24  
    1.25    def string(obj: T, name: String): Option[String] =
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/General/uuid.scala	Thu Dec 13 15:21:34 2018 +0100
     2.3 @@ -0,0 +1,20 @@
     2.4 +/*  Title:      Pure/General/uuid.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Universally unique identifiers.
     2.8 +*/
     2.9 +
    2.10 +package isabelle
    2.11 +
    2.12 +
    2.13 +object UUID
    2.14 +{
    2.15 +  type T = java.util.UUID
    2.16 +
    2.17 +  def random(): T = java.util.UUID.randomUUID()
    2.18 +  def random_string(): String = random().toString
    2.19 +
    2.20 +  def unapply(s: String): Option[T] =
    2.21 +    try { Some(java.util.UUID.fromString(s)) }
    2.22 +    catch { case _: IllegalArgumentException => None }
    2.23 +}
     3.1 --- a/src/Pure/PIDE/headless.scala	Thu Dec 13 13:11:35 2018 +0100
     3.2 +++ b/src/Pure/PIDE/headless.scala	Thu Dec 13 15:21:34 2018 +0100
     3.3 @@ -193,7 +193,7 @@
     3.4        check_limit: Int = 0,
     3.5        watchdog_timeout: Time = default_watchdog_timeout,
     3.6        nodes_status_delay: Time = default_nodes_status_delay,
     3.7 -      id: UUID = UUID(),
     3.8 +      id: UUID.T = UUID.random(),
     3.9        // commit: must not block, must not fail
    3.10        commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None,
    3.11        commit_cleanup_delay: Time = default_commit_cleanup_delay,
    3.12 @@ -362,7 +362,7 @@
    3.13      }
    3.14  
    3.15      sealed case class State(
    3.16 -      required: Multi_Map[Document.Node.Name, UUID] = Multi_Map.empty,
    3.17 +      required: Multi_Map[Document.Node.Name, UUID.T] = Multi_Map.empty,
    3.18        theories: Map[Document.Node.Name, Theory] = Map.empty)
    3.19      {
    3.20        lazy val theory_graph: Graph[Document.Node.Name, Unit] =
    3.21 @@ -375,10 +375,10 @@
    3.22  
    3.23        def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name)
    3.24  
    3.25 -      def insert_required(id: UUID, names: List[Document.Node.Name]): State =
    3.26 +      def insert_required(id: UUID.T, names: List[Document.Node.Name]): State =
    3.27          copy(required = (required /: names)(_.insert(_, id)))
    3.28  
    3.29 -      def remove_required(id: UUID, names: List[Document.Node.Name]): State =
    3.30 +      def remove_required(id: UUID.T, names: List[Document.Node.Name]): State =
    3.31          copy(required = (required /: names)(_.remove(_, id)))
    3.32  
    3.33        def update_theories(update: List[(Document.Node.Name, Theory)]): State =
    3.34 @@ -396,7 +396,8 @@
    3.35          copy(theories = theories -- remove)
    3.36        }
    3.37  
    3.38 -      def unload_theories(session: Session, id: UUID, dep_theories: List[Document.Node.Name]): State =
    3.39 +      def unload_theories(session: Session, id: UUID.T, dep_theories: List[Document.Node.Name])
    3.40 +        : State =
    3.41        {
    3.42          val st1 = remove_required(id, dep_theories)
    3.43          val theory_edits =
    3.44 @@ -455,7 +456,7 @@
    3.45  
    3.46      def load_theories(
    3.47        session: Session,
    3.48 -      id: UUID,
    3.49 +      id: UUID.T,
    3.50        dep_theories: List[Document.Node.Name],
    3.51        progress: Progress)
    3.52      {
    3.53 @@ -490,12 +491,12 @@
    3.54          })
    3.55      }
    3.56  
    3.57 -    def unload_theories(session: Session, id: UUID, dep_theories: List[Document.Node.Name])
    3.58 +    def unload_theories(session: Session, id: UUID.T, dep_theories: List[Document.Node.Name])
    3.59      {
    3.60        state.change(_.unload_theories(session, id, dep_theories))
    3.61      }
    3.62  
    3.63 -    def clean_theories(session: Session, id: UUID, clean: Set[Document.Node.Name])
    3.64 +    def clean_theories(session: Session, id: UUID.T, clean: Set[Document.Node.Name])
    3.65      {
    3.66        state.change(st =>
    3.67          {
     4.1 --- a/src/Pure/ROOT.scala	Thu Dec 13 13:11:35 2018 +0100
     4.2 +++ b/src/Pure/ROOT.scala	Thu Dec 13 15:21:34 2018 +0100
     4.3 @@ -21,7 +21,4 @@
     4.4    def proper[A](x: A): Option[A] = Library.proper(x)
     4.5    val proper_string = Library.proper_string _
     4.6    def proper_list[A](list: List[A]): Option[List[A]] = Library.proper_list(list)
     4.7 -
     4.8 -  type UUID = java.util.UUID
     4.9 -  def UUID(): UUID = java.util.UUID.randomUUID()
    4.10  }
     5.1 --- a/src/Pure/Tools/server.scala	Thu Dec 13 13:11:35 2018 +0100
     5.2 +++ b/src/Pure/Tools/server.scala	Thu Dec 13 15:21:34 2018 +0100
     5.3 @@ -238,7 +238,7 @@
     5.4      def remove_task(task: Task): Unit =
     5.5        _tasks.change(_ - task)
     5.6  
     5.7 -    def cancel_task(id: UUID): Unit =
     5.8 +    def cancel_task(id: UUID.T): Unit =
     5.9        _tasks.change(tasks => { tasks.find(task => task.id == id).foreach(_.cancel); tasks })
    5.10  
    5.11      def close()
    5.12 @@ -282,7 +282,7 @@
    5.13    {
    5.14      task =>
    5.15  
    5.16 -    val id: UUID = UUID()
    5.17 +    val id: UUID.T = UUID.random()
    5.18      val ident: JSON.Object.Entry = ("task" -> id.toString)
    5.19  
    5.20      val progress: Connection_Progress = context.progress(ident)
    5.21 @@ -492,11 +492,11 @@
    5.22  
    5.23    private val server_socket = new ServerSocket(_port, 50, InetAddress.getByName("127.0.0.1"))
    5.24  
    5.25 -  private val _sessions = Synchronized(Map.empty[UUID, Headless.Session])
    5.26 -  def err_session(id: UUID): Nothing = error("No session " + Library.single_quote(id.toString))
    5.27 -  def the_session(id: UUID): Headless.Session = _sessions.value.get(id) getOrElse err_session(id)
    5.28 -  def add_session(entry: (UUID, Headless.Session)) { _sessions.change(_ + entry) }
    5.29 -  def remove_session(id: UUID): Headless.Session =
    5.30 +  private val _sessions = Synchronized(Map.empty[UUID.T, Headless.Session])
    5.31 +  def err_session(id: UUID.T): Nothing = error("No session " + Library.single_quote(id.toString))
    5.32 +  def the_session(id: UUID.T): Headless.Session = _sessions.value.get(id) getOrElse err_session(id)
    5.33 +  def add_session(entry: (UUID.T, Headless.Session)) { _sessions.change(_ + entry) }
    5.34 +  def remove_session(id: UUID.T): Headless.Session =
    5.35    {
    5.36      _sessions.change_result(sessions =>
    5.37        sessions.get(id) match {
    5.38 @@ -520,7 +520,7 @@
    5.39    }
    5.40  
    5.41    def port: Int = server_socket.getLocalPort
    5.42 -  val password: String = UUID().toString
    5.43 +  val password: String = UUID.random_string()
    5.44  
    5.45    override def toString: String = Server.print(port, password)
    5.46  
     6.1 --- a/src/Pure/Tools/server_commands.scala	Thu Dec 13 13:11:35 2018 +0100
     6.2 +++ b/src/Pure/Tools/server_commands.scala	Thu Dec 13 15:21:34 2018 +0100
     6.3 @@ -13,7 +13,7 @@
     6.4  
     6.5    object Cancel
     6.6    {
     6.7 -    sealed case class Args(task: UUID)
     6.8 +    sealed case class Args(task: UUID.T)
     6.9  
    6.10      def unapply(json: JSON.T): Option[Args] =
    6.11        for { task <- JSON.uuid(json, "task") }
    6.12 @@ -107,7 +107,7 @@
    6.13        yield Args(build = build, print_mode = print_mode)
    6.14  
    6.15      def command(args: Args, progress: Progress = No_Progress, log: Logger = No_Logger)
    6.16 -      : (JSON.Object.T, (UUID, Headless.Session)) =
    6.17 +      : (JSON.Object.T, (UUID.T, Headless.Session)) =
    6.18      {
    6.19        val base_info =
    6.20          try { Session_Build.command(args.build, progress = progress)._3 }
    6.21 @@ -123,7 +123,7 @@
    6.22            progress = progress,
    6.23            log = log)
    6.24  
    6.25 -      val id = UUID()
    6.26 +      val id = UUID.random()
    6.27  
    6.28        val res =
    6.29          JSON.Object(
    6.30 @@ -136,7 +136,7 @@
    6.31  
    6.32    object Session_Stop
    6.33    {
    6.34 -    def unapply(json: JSON.T): Option[UUID] =
    6.35 +    def unapply(json: JSON.T): Option[UUID.T] =
    6.36        JSON.uuid(json, "session_id")
    6.37  
    6.38      def command(session: Headless.Session): (JSON.Object.T, Process_Result) =
    6.39 @@ -152,7 +152,7 @@
    6.40    object Use_Theories
    6.41    {
    6.42      sealed case class Args(
    6.43 -      session_id: UUID,
    6.44 +      session_id: UUID.T,
    6.45        theories: List[String],
    6.46        master_dir: String = "",
    6.47        pretty_margin: Double = Pretty.default_margin,
    6.48 @@ -187,7 +187,7 @@
    6.49  
    6.50      def command(args: Args,
    6.51        session: Headless.Session,
    6.52 -      id: UUID = UUID(),
    6.53 +      id: UUID.T = UUID.random(),
    6.54        progress: Progress = No_Progress): (JSON.Object.T, Headless.Use_Theories_Result) =
    6.55      {
    6.56        val result =
    6.57 @@ -249,7 +249,7 @@
    6.58    object Purge_Theories
    6.59    {
    6.60      sealed case class Args(
    6.61 -      session_id: UUID,
    6.62 +      session_id: UUID.T,
    6.63        theories: List[String] = Nil,
    6.64        master_dir: String = "",
    6.65        all: Boolean = false)
     7.1 --- a/src/Pure/build-jars	Thu Dec 13 13:11:35 2018 +0100
     7.2 +++ b/src/Pure/build-jars	Thu Dec 13 15:21:34 2018 +0100
     7.3 @@ -75,6 +75,7 @@
     7.4    General/untyped.scala
     7.5    General/url.scala
     7.6    General/utf8.scala
     7.7 +  General/uuid.scala
     7.8    General/value.scala
     7.9    General/word.scala
    7.10    General/xz.scala
     8.1 --- a/src/Tools/VSCode/src/grammar.scala	Thu Dec 13 13:11:35 2018 +0100
     8.2 +++ b/src/Tools/VSCode/src/grammar.scala	Thu Dec 13 15:21:34 2018 +0100
     8.3 @@ -45,7 +45,7 @@
     8.4    "name": "Isabelle",
     8.5    "scopeName": "source.isabelle",
     8.6    "fileTypes": ["thy"],
     8.7 -  "uuid": """ + JSON.Format(UUID().toString) + """,
     8.8 +  "uuid": """ + JSON.Format(UUID.random_string()) + """,
     8.9    "repository": {
    8.10      "comment": {
    8.11        "patterns": [
     9.1 --- a/src/Tools/jEdit/src/plugin.scala	Thu Dec 13 13:11:35 2018 +0100
     9.2 +++ b/src/Tools/jEdit/src/plugin.scala	Thu Dec 13 15:21:34 2018 +0100
     9.3 @@ -433,7 +433,7 @@
     9.4  
     9.5    /* HTTP server */
     9.6  
     9.7 -  val http_root: String = "/" + UUID()
     9.8 +  val http_root: String = "/" + UUID.random()
     9.9  
    9.10    val http_server: HTTP.Server = HTTP.server(Document_Model.http_handlers(http_root))
    9.11