# HG changeset patch
# User wenzelm
# Date 1502033934 -7200
# Node ID 95847ffa62dcd87ff6ac0dd24621c5ea264ddab4
# Parent  66331026a2fc7951092dd4795775b748e4aae587
tuned signature;

diff -r 66331026a2fc -r 95847ffa62dc src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Sun Aug 06 17:32:32 2017 +0200
+++ b/src/Pure/Tools/server.scala	Sun Aug 06 17:38:54 2017 +0200
@@ -7,7 +7,6 @@
 package isabelle
 
 
-import java.util.UUID
 import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter}
 import java.net.{Socket, ServerSocket, InetAddress}
 
@@ -132,7 +131,7 @@
   def port: Int = server_socket.getLocalPort
   def close { server_socket.close }
 
-  val password: String = proper_string(_password) getOrElse UUID.randomUUID().toString
+  val password: String = proper_string(_password) getOrElse Library.UUID()
 
   private def handle_connection(socket: Socket)
   {
diff -r 66331026a2fc -r 95847ffa62dc src/Pure/library.scala
--- a/src/Pure/library.scala	Sun Aug 06 17:32:32 2017 +0200
+++ b/src/Pure/library.scala	Sun Aug 06 17:38:54 2017 +0200
@@ -259,4 +259,9 @@
 
   def proper_list[A](list: List[A]): Option[List[A]] =
     if (list == null || list.isEmpty) None else Some(list)
+
+
+  /* UUID */
+
+  def UUID(): String = java.util.UUID.randomUUID().toString
 }
diff -r 66331026a2fc -r 95847ffa62dc src/Tools/VSCode/src/grammar.scala
--- a/src/Tools/VSCode/src/grammar.scala	Sun Aug 06 17:32:32 2017 +0200
+++ b/src/Tools/VSCode/src/grammar.scala	Sun Aug 06 17:38:54 2017 +0200
@@ -9,8 +9,6 @@
 
 import isabelle._
 
-import java.util.UUID
-
 
 object Grammar
 {
@@ -47,7 +45,7 @@
   "name": "Isabelle",
   "scopeName": "source.isabelle",
   "fileTypes": ["thy"],
-  "uuid": """ + JSON.Format(UUID.randomUUID().toString) + """,
+  "uuid": """ + JSON.Format(Library.UUID()) + """,
   "repository": {
     "comment": {
       "patterns": [
diff -r 66331026a2fc -r 95847ffa62dc src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Sun Aug 06 17:32:32 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Sun Aug 06 17:38:54 2017 +0200
@@ -12,7 +12,6 @@
 import javax.swing.JOptionPane
 
 import java.io.{File => JFile}
-import java.util.UUID
 
 import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug, PerspectiveManager}
 import org.gjt.sp.jedit.textarea.JEditTextArea
@@ -398,7 +397,7 @@
 
   /* HTTP server */
 
-  val http_root: String = "/" + UUID.randomUUID().toString
+  val http_root: String = "/" + Library.UUID()
 
   val http_server: HTTP.Server = HTTP.server(Document_Model.http_handlers(http_root))