clarified modules;

--- a/src/Pure/Concurrent/standard_thread.scala	Mon Sep 05 21:09:50 2016 +0200
+++ b/src/Pure/Concurrent/standard_thread.scala	Mon Sep 05 22:09:52 2016 +0200
@@ -31,7 +31,7 @@
 
   lazy val pool: ThreadPoolExecutor =
     {
-      val m = Properties.Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
+      val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
       val n = if (m > 0) m else (Runtime.getRuntime.availableProcessors max 1) min 8
       val executor =
         new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable])

--- a/src/Pure/General/properties.scala	Mon Sep 05 21:09:50 2016 +0200
+++ b/src/Pure/General/properties.scala	Mon Sep 05 22:09:52 2016 +0200
@@ -10,55 +10,6 @@
 
 object Properties
 {
-  /* plain values */
-
-  object Value
-  {
-    object Boolean
-    {
-      def apply(x: scala.Boolean): java.lang.String = x.toString
-      def unapply(s: java.lang.String): Option[scala.Boolean] =
-        s match {
-          case "true" => Some(true)
-          case "false" => Some(false)
-          case _ => None
-        }
-      def parse(s: java.lang.String): scala.Boolean =
-        unapply(s) getOrElse error("Bad boolean: " + quote(s))
-    }
-
-    object Int
-    {
-      def apply(x: scala.Int): java.lang.String = Library.signed_string_of_int(x)
-      def unapply(s: java.lang.String): Option[scala.Int] =
-        try { Some(Integer.parseInt(s)) }
-        catch { case _: NumberFormatException => None }
-      def parse(s: java.lang.String): scala.Int =
-        unapply(s) getOrElse error("Bad integer: " + quote(s))
-    }
-
-    object Long
-    {
-      def apply(x: scala.Long): java.lang.String = Library.signed_string_of_long(x)
-      def unapply(s: java.lang.String): Option[scala.Long] =
-        try { Some(java.lang.Long.parseLong(s)) }
-        catch { case _: NumberFormatException => None }
-      def parse(s: java.lang.String): scala.Long =
-        unapply(s) getOrElse error("Bad integer: " + quote(s))
-    }
-
-    object Double
-    {
-      def apply(x: scala.Double): java.lang.String = x.toString
-      def unapply(s: java.lang.String): Option[scala.Double] =
-        try { Some(java.lang.Double.parseDouble(s)) }
-        catch { case _: NumberFormatException => None }
-      def parse(s: java.lang.String): scala.Double =
-        unapply(s) getOrElse error("Bad real: " + quote(s))
-    }
-  }
-
-
   /* named entries */
 
   type Entry = (java.lang.String, java.lang.String)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/value.scala	Mon Sep 05 22:09:52 2016 +0200
@@ -0,0 +1,54 @@
+/*  Title:      Pure/General/value.scala
+    Author:     Makarius
+
+Plain values, represented as string.
+*/
+
+package isabelle
+
+
+object Value
+{
+  object Boolean
+  {
+    def apply(x: scala.Boolean): java.lang.String = x.toString
+    def unapply(s: java.lang.String): Option[scala.Boolean] =
+      s match {
+        case "true" => Some(true)
+        case "false" => Some(false)
+        case _ => None
+      }
+    def parse(s: java.lang.String): scala.Boolean =
+      unapply(s) getOrElse error("Bad boolean: " + quote(s))
+  }
+
+  object Int
+  {
+    def apply(x: scala.Int): java.lang.String = Library.signed_string_of_int(x)
+    def unapply(s: java.lang.String): Option[scala.Int] =
+      try { Some(Integer.parseInt(s)) }
+      catch { case _: NumberFormatException => None }
+    def parse(s: java.lang.String): scala.Int =
+      unapply(s) getOrElse error("Bad integer: " + quote(s))
+  }
+
+  object Long
+  {
+    def apply(x: scala.Long): java.lang.String = Library.signed_string_of_long(x)
+    def unapply(s: java.lang.String): Option[scala.Long] =
+      try { Some(java.lang.Long.parseLong(s)) }
+      catch { case _: NumberFormatException => None }
+    def parse(s: java.lang.String): scala.Long =
+      unapply(s) getOrElse error("Bad integer: " + quote(s))
+  }
+
+  object Double
+  {
+    def apply(x: scala.Double): java.lang.String = x.toString
+    def unapply(s: java.lang.String): Option[scala.Double] =
+      try { Some(java.lang.Double.parseDouble(s)) }
+      catch { case _: NumberFormatException => None }
+    def parse(s: java.lang.String): scala.Double =
+      unapply(s) getOrElse error("Bad real: " + quote(s))
+  }
+}

--- a/src/Pure/ML/ml_syntax.scala	Mon Sep 05 21:09:50 2016 +0200
+++ b/src/Pure/ML/ml_syntax.scala	Mon Sep 05 22:09:52 2016 +0200
@@ -14,8 +14,8 @@
   private def signed_int(s: String): String =
     if (s(0) == '-') "~" + s.substring(1) else s
 
-  def print_int(i: Int): String = signed_int(Properties.Value.Int(i))
-  def print_long(i: Long): String = signed_int(Properties.Value.Long(i))
+  def print_int(i: Int): String = signed_int(Value.Int(i))
+  def print_long(i: Long): String = signed_int(Value.Long(i))
 
 
   /* string */

--- a/src/Pure/PIDE/document_id.scala	Mon Sep 05 21:09:50 2016 +0200
+++ b/src/Pure/PIDE/document_id.scala	Mon Sep 05 22:09:52 2016 +0200
@@ -20,7 +20,7 @@
   val none: Generic = 0
   val make = Counter.make()
 
-  def apply(id: Generic): String = Properties.Value.Long.apply(id)
-  def unapply(s: String): Option[Generic] = Properties.Value.Long.unapply(s)
+  def apply(id: Generic): String = Value.Long.apply(id)
+  def unapply(s: String): Option[Generic] = Value.Long.unapply(s)
 }
 

--- a/src/Pure/PIDE/protocol.scala	Mon Sep 05 21:09:50 2016 +0200
+++ b/src/Pure/PIDE/protocol.scala	Mon Sep 05 22:09:52 2016 +0200
@@ -404,7 +404,7 @@
   /* dialog via document content */
 
   def dialog_result(serial: Long, result: String): Unit =
-    protocol_command("Document.dialog_result", Properties.Value.Long(serial), result)
+    protocol_command("Document.dialog_result", Value.Long(serial), result)
 
 
   /* build_theories */

--- a/src/Pure/PIDE/query_operation.scala	Mon Sep 05 21:09:50 2016 +0200
+++ b/src/Pure/PIDE/query_operation.scala	Mon Sep 05 22:09:52 2016 +0200
@@ -105,8 +105,8 @@
               case XML.Elem(Markup(Markup.SENDBACK, props), b) =>
                 val props1 =
                   props.map({
-                    case (Markup.ID, Properties.Value.Long(id)) if id == state0.exec_id =>
-                      (Markup.ID, Properties.Value.Long(command.id))
+                    case (Markup.ID, Value.Long(id)) if id == state0.exec_id =>
+                      (Markup.ID, Value.Long(command.id))
                     case p => p
                   })
                 XML.Elem(Markup(Markup.SENDBACK, props1), resolve(b))

--- a/src/Pure/System/bash.scala	Mon Sep 05 21:09:50 2016 +0200
+++ b/src/Pure/System/bash.scala	Mon Sep 05 22:09:52 2016 +0200
@@ -124,7 +124,7 @@
           if (timing_file.isFile) {
             val t =
               Word.explode(File.read(timing_file)) match {
-                case List(Properties.Value.Long(elapsed), Properties.Value.Long(cpu)) =>
+                case List(Value.Long(elapsed), Value.Long(cpu)) =>
                   Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero)
                 case _ => Timing.zero
               }

--- a/src/Pure/System/options.scala	Mon Sep 05 21:09:50 2016 +0200
+++ b/src/Pure/System/options.scala	Mon Sep 05 22:09:52 2016 +0200
@@ -250,25 +250,25 @@
 
   class Bool_Access
   {
-    def apply(name: String): Boolean = get(name, Options.Bool, Properties.Value.Boolean.unapply)
+    def apply(name: String): Boolean = get(name, Options.Bool, Value.Boolean.unapply)
     def update(name: String, x: Boolean): Options =
-      put(name, Options.Bool, Properties.Value.Boolean(x))
+      put(name, Options.Bool, Value.Boolean(x))
   }
   val bool = new Bool_Access
 
   class Int_Access
   {
-    def apply(name: String): Int = get(name, Options.Int, Properties.Value.Int.unapply)
+    def apply(name: String): Int = get(name, Options.Int, Value.Int.unapply)
     def update(name: String, x: Int): Options =
-      put(name, Options.Int, Properties.Value.Int(x))
+      put(name, Options.Int, Value.Int(x))
   }
   val int = new Int_Access
 
   class Real_Access
   {
-    def apply(name: String): Double = get(name, Options.Real, Properties.Value.Double.unapply)
+    def apply(name: String): Double = get(name, Options.Real, Value.Double.unapply)
     def update(name: String, x: Double): Options =
-      put(name, Options.Real, Properties.Value.Double(x))
+      put(name, Options.Real, Value.Double(x))
   }
   val real = new Real_Access
 

--- a/src/Pure/Tools/build.scala	Mon Sep 05 21:09:50 2016 +0200
+++ b/src/Pure/Tools/build.scala	Mon Sep 05 22:09:52 2016 +0200
@@ -790,7 +790,7 @@
       "c" -> (_ => clean_build = true),
       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
       "g:" -> (arg => session_groups = session_groups ::: List(arg)),
-      "j:" -> (arg => max_jobs = Properties.Value.Int.parse(arg)),
+      "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
       "k:" -> (arg => check_keywords = check_keywords + arg),
       "l" -> (_ => list_files = true),
       "n" -> (_ => no_build = true),

--- a/src/Pure/Tools/build_doc.scala	Mon Sep 05 21:09:50 2016 +0200
+++ b/src/Pure/Tools/build_doc.scala	Mon Sep 05 22:09:52 2016 +0200
@@ -88,7 +88,7 @@
   suitable document_variants entry.
 """,
       "a" -> (_ => all_docs = true),
-      "j:" -> (arg => max_jobs = Properties.Value.Int.parse(arg)),
+      "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
       "s" -> (_ => system_mode = true))
 
     val docs = getopts(args)

--- a/src/Pure/Tools/build_stats.scala	Mon Sep 05 21:09:50 2016 +0200
+++ b/src/Pure/Tools/build_stats.scala	Mon Sep 05 22:09:52 2016 +0200
@@ -38,8 +38,6 @@
 
   def parse(text: String): Build_Stats =
   {
-    import Properties.Value
-
     val ml_options = new mutable.ListBuffer[(String, String)]
     var finished = Map.empty[String, Timing]
     var timing = Map.empty[String, Timing]
@@ -208,11 +206,11 @@
         "D:" -> (arg => target_dir = Path.explode(arg)),
         "M" -> (_ => ml_timing = Some(true)),
         "S:" -> (arg => only_sessions = space_explode(',', arg).toSet),
-        "T:" -> (arg => elapsed_threshold = Time.minutes(Properties.Value.Double.parse(arg))),
-        "l:" -> (arg => history_length = Properties.Value.Int.parse(arg)),
+        "T:" -> (arg => elapsed_threshold = Time.minutes(Value.Double.parse(arg))),
+        "l:" -> (arg => history_length = Value.Int.parse(arg)),
         "m" -> (_ => ml_timing = Some(false)),
         "s:" -> (arg =>
-          space_explode('x', arg).map(Properties.Value.Int.parse(_)) match {
+          space_explode('x', arg).map(Value.Int.parse(_)) match {
             case List(w, h) if w > 0 && h > 0 => size = (w, h)
             case _ => error("Error bad PNG image size: " + quote(arg))
           }))

--- a/src/Pure/Tools/debugger.scala	Mon Sep 05 21:09:50 2016 +0200
+++ b/src/Pure/Tools/debugger.scala	Mon Sep 05 22:09:52 2016 +0200
@@ -234,8 +234,8 @@
         "Debugger.breakpoint",
         Symbol.encode(command.node_name.node),
         Document_ID(command.id),
-        Properties.Value.Long(breakpoint),
-        Properties.Value.Boolean(breakpoint_state))
+        Value.Long(breakpoint),
+        Value.Boolean(breakpoint_state))
       state1
     })
   }

--- a/src/Pure/Tools/simplifier_trace.scala	Mon Sep 05 21:09:50 2016 +0200
+++ b/src/Pure/Tools/simplifier_trace.scala	Mon Sep 05 22:09:52 2016 +0200
@@ -165,7 +165,7 @@
     def do_reply(session: Session, serial: Long, answer: Answer)
     {
       session.protocol_command(
-        "Simplifier_Trace.reply", Properties.Value.Long(serial), answer.name)
+        "Simplifier_Trace.reply", Value.Long(serial), answer.name)
     }
 
     Consumer_Thread.fork[Any]("Simplifier_Trace.manager", daemon = true)(

--- a/src/Pure/build-jars	Mon Sep 05 21:09:50 2016 +0200
+++ b/src/Pure/build-jars	Mon Sep 05 22:09:52 2016 +0200
@@ -50,6 +50,7 @@
   General/timing.scala
   General/untyped.scala
   General/url.scala
+  General/value.scala
   General/word.scala
   General/xz_file.scala
   Isar/document_structure.scala

--- a/src/Tools/jEdit/src/monitor_dockable.scala	Mon Sep 05 21:09:50 2016 +0200
+++ b/src/Tools/jEdit/src/monitor_dockable.scala	Mon Sep 05 22:09:52 2016 +0200
@@ -33,7 +33,7 @@
     statistics = statistics.enqueue(stats)
     statistics_length += 1
     limit_data.text match {
-      case Properties.Value.Int(limit) =>
+      case Value.Int(limit) =>
         while (statistics_length > limit) {
           statistics = statistics.dequeue._2
           statistics_length -= 1
@@ -91,7 +91,7 @@
   private val limit_data = new TextField("200", 5) {
     tooltip = "Limit for accumulated data"
     verifier = (s: String) =>
-      s match { case Properties.Value.Int(x) => x > 0 case _ => false }
+      s match { case Value.Int(x) => x > 0 case _ => false }
     reactions += { case ValueChanged(_) => input_delay.invoke() }
   }
 

--- a/src/Tools/jEdit/src/query_dockable.scala	Mon Sep 05 21:09:50 2016 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala	Mon Sep 05 22:09:52 2016 +0200
@@ -102,7 +102,7 @@
     private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
       tooltip = "Limit of displayed results"
       verifier = (s: String) =>
-        s match { case Properties.Value.Int(x) => x >= 0 case _ => false }
+        s match { case Value.Int(x) => x >= 0 case _ => false }
       listenTo(keys)
       reactions += { case KeyPressed(_, Key.Enter, 0, _) => apply_query() }
     }

--- a/src/Tools/jEdit/src/timing_dockable.scala	Mon Sep 05 21:09:50 2016 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Mon Sep 05 22:09:52 2016 +0200
@@ -132,14 +132,14 @@
     reactions += {
       case _: ValueChanged =>
         text match {
-          case Properties.Value.Double(x) if x >= 0.0 => timing_threshold = x
+          case Value.Double(x) if x >= 0.0 => timing_threshold = x
           case _ =>
         }
         handle_update()
     }
     tooltip = threshold_tooltip
     verifier = ((s: String) =>
-      s match { case Properties.Value.Double(x) => x >= 0.0 case _ => false })
+      s match { case Value.Double(x) => x >= 0.0 case _ => false })
   }
 
   private val controls =