clarified modules;
authorwenzelm
Mon Sep 05 22:09:52 2016 +0200 (2016-09-05)
changeset 63805c272680df665
parent 63804 70554522bf98
child 63806 c54a53ef1873
clarified modules;
src/Pure/Concurrent/standard_thread.scala
src/Pure/General/properties.scala
src/Pure/General/value.scala
src/Pure/ML/ml_syntax.scala
src/Pure/PIDE/document_id.scala
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/query_operation.scala
src/Pure/System/bash.scala
src/Pure/System/options.scala
src/Pure/Tools/build.scala
src/Pure/Tools/build_doc.scala
src/Pure/Tools/build_stats.scala
src/Pure/Tools/debugger.scala
src/Pure/Tools/simplifier_trace.scala
src/Pure/build-jars
src/Tools/jEdit/src/monitor_dockable.scala
src/Tools/jEdit/src/query_dockable.scala
src/Tools/jEdit/src/timing_dockable.scala
     1.1 --- a/src/Pure/Concurrent/standard_thread.scala	Mon Sep 05 21:09:50 2016 +0200
     1.2 +++ b/src/Pure/Concurrent/standard_thread.scala	Mon Sep 05 22:09:52 2016 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4  
     1.5    lazy val pool: ThreadPoolExecutor =
     1.6      {
     1.7 -      val m = Properties.Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
     1.8 +      val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
     1.9        val n = if (m > 0) m else (Runtime.getRuntime.availableProcessors max 1) min 8
    1.10        val executor =
    1.11          new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable])
     2.1 --- a/src/Pure/General/properties.scala	Mon Sep 05 21:09:50 2016 +0200
     2.2 +++ b/src/Pure/General/properties.scala	Mon Sep 05 22:09:52 2016 +0200
     2.3 @@ -10,55 +10,6 @@
     2.4  
     2.5  object Properties
     2.6  {
     2.7 -  /* plain values */
     2.8 -
     2.9 -  object Value
    2.10 -  {
    2.11 -    object Boolean
    2.12 -    {
    2.13 -      def apply(x: scala.Boolean): java.lang.String = x.toString
    2.14 -      def unapply(s: java.lang.String): Option[scala.Boolean] =
    2.15 -        s match {
    2.16 -          case "true" => Some(true)
    2.17 -          case "false" => Some(false)
    2.18 -          case _ => None
    2.19 -        }
    2.20 -      def parse(s: java.lang.String): scala.Boolean =
    2.21 -        unapply(s) getOrElse error("Bad boolean: " + quote(s))
    2.22 -    }
    2.23 -
    2.24 -    object Int
    2.25 -    {
    2.26 -      def apply(x: scala.Int): java.lang.String = Library.signed_string_of_int(x)
    2.27 -      def unapply(s: java.lang.String): Option[scala.Int] =
    2.28 -        try { Some(Integer.parseInt(s)) }
    2.29 -        catch { case _: NumberFormatException => None }
    2.30 -      def parse(s: java.lang.String): scala.Int =
    2.31 -        unapply(s) getOrElse error("Bad integer: " + quote(s))
    2.32 -    }
    2.33 -
    2.34 -    object Long
    2.35 -    {
    2.36 -      def apply(x: scala.Long): java.lang.String = Library.signed_string_of_long(x)
    2.37 -      def unapply(s: java.lang.String): Option[scala.Long] =
    2.38 -        try { Some(java.lang.Long.parseLong(s)) }
    2.39 -        catch { case _: NumberFormatException => None }
    2.40 -      def parse(s: java.lang.String): scala.Long =
    2.41 -        unapply(s) getOrElse error("Bad integer: " + quote(s))
    2.42 -    }
    2.43 -
    2.44 -    object Double
    2.45 -    {
    2.46 -      def apply(x: scala.Double): java.lang.String = x.toString
    2.47 -      def unapply(s: java.lang.String): Option[scala.Double] =
    2.48 -        try { Some(java.lang.Double.parseDouble(s)) }
    2.49 -        catch { case _: NumberFormatException => None }
    2.50 -      def parse(s: java.lang.String): scala.Double =
    2.51 -        unapply(s) getOrElse error("Bad real: " + quote(s))
    2.52 -    }
    2.53 -  }
    2.54 -
    2.55 -
    2.56    /* named entries */
    2.57  
    2.58    type Entry = (java.lang.String, java.lang.String)
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/General/value.scala	Mon Sep 05 22:09:52 2016 +0200
     3.3 @@ -0,0 +1,54 @@
     3.4 +/*  Title:      Pure/General/value.scala
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Plain values, represented as string.
     3.8 +*/
     3.9 +
    3.10 +package isabelle
    3.11 +
    3.12 +
    3.13 +object Value
    3.14 +{
    3.15 +  object Boolean
    3.16 +  {
    3.17 +    def apply(x: scala.Boolean): java.lang.String = x.toString
    3.18 +    def unapply(s: java.lang.String): Option[scala.Boolean] =
    3.19 +      s match {
    3.20 +        case "true" => Some(true)
    3.21 +        case "false" => Some(false)
    3.22 +        case _ => None
    3.23 +      }
    3.24 +    def parse(s: java.lang.String): scala.Boolean =
    3.25 +      unapply(s) getOrElse error("Bad boolean: " + quote(s))
    3.26 +  }
    3.27 +
    3.28 +  object Int
    3.29 +  {
    3.30 +    def apply(x: scala.Int): java.lang.String = Library.signed_string_of_int(x)
    3.31 +    def unapply(s: java.lang.String): Option[scala.Int] =
    3.32 +      try { Some(Integer.parseInt(s)) }
    3.33 +      catch { case _: NumberFormatException => None }
    3.34 +    def parse(s: java.lang.String): scala.Int =
    3.35 +      unapply(s) getOrElse error("Bad integer: " + quote(s))
    3.36 +  }
    3.37 +
    3.38 +  object Long
    3.39 +  {
    3.40 +    def apply(x: scala.Long): java.lang.String = Library.signed_string_of_long(x)
    3.41 +    def unapply(s: java.lang.String): Option[scala.Long] =
    3.42 +      try { Some(java.lang.Long.parseLong(s)) }
    3.43 +      catch { case _: NumberFormatException => None }
    3.44 +    def parse(s: java.lang.String): scala.Long =
    3.45 +      unapply(s) getOrElse error("Bad integer: " + quote(s))
    3.46 +  }
    3.47 +
    3.48 +  object Double
    3.49 +  {
    3.50 +    def apply(x: scala.Double): java.lang.String = x.toString
    3.51 +    def unapply(s: java.lang.String): Option[scala.Double] =
    3.52 +      try { Some(java.lang.Double.parseDouble(s)) }
    3.53 +      catch { case _: NumberFormatException => None }
    3.54 +    def parse(s: java.lang.String): scala.Double =
    3.55 +      unapply(s) getOrElse error("Bad real: " + quote(s))
    3.56 +  }
    3.57 +}
     4.1 --- a/src/Pure/ML/ml_syntax.scala	Mon Sep 05 21:09:50 2016 +0200
     4.2 +++ b/src/Pure/ML/ml_syntax.scala	Mon Sep 05 22:09:52 2016 +0200
     4.3 @@ -14,8 +14,8 @@
     4.4    private def signed_int(s: String): String =
     4.5      if (s(0) == '-') "~" + s.substring(1) else s
     4.6  
     4.7 -  def print_int(i: Int): String = signed_int(Properties.Value.Int(i))
     4.8 -  def print_long(i: Long): String = signed_int(Properties.Value.Long(i))
     4.9 +  def print_int(i: Int): String = signed_int(Value.Int(i))
    4.10 +  def print_long(i: Long): String = signed_int(Value.Long(i))
    4.11  
    4.12  
    4.13    /* string */
     5.1 --- a/src/Pure/PIDE/document_id.scala	Mon Sep 05 21:09:50 2016 +0200
     5.2 +++ b/src/Pure/PIDE/document_id.scala	Mon Sep 05 22:09:52 2016 +0200
     5.3 @@ -20,7 +20,7 @@
     5.4    val none: Generic = 0
     5.5    val make = Counter.make()
     5.6  
     5.7 -  def apply(id: Generic): String = Properties.Value.Long.apply(id)
     5.8 -  def unapply(s: String): Option[Generic] = Properties.Value.Long.unapply(s)
     5.9 +  def apply(id: Generic): String = Value.Long.apply(id)
    5.10 +  def unapply(s: String): Option[Generic] = Value.Long.unapply(s)
    5.11  }
    5.12  
     6.1 --- a/src/Pure/PIDE/protocol.scala	Mon Sep 05 21:09:50 2016 +0200
     6.2 +++ b/src/Pure/PIDE/protocol.scala	Mon Sep 05 22:09:52 2016 +0200
     6.3 @@ -404,7 +404,7 @@
     6.4    /* dialog via document content */
     6.5  
     6.6    def dialog_result(serial: Long, result: String): Unit =
     6.7 -    protocol_command("Document.dialog_result", Properties.Value.Long(serial), result)
     6.8 +    protocol_command("Document.dialog_result", Value.Long(serial), result)
     6.9  
    6.10  
    6.11    /* build_theories */
     7.1 --- a/src/Pure/PIDE/query_operation.scala	Mon Sep 05 21:09:50 2016 +0200
     7.2 +++ b/src/Pure/PIDE/query_operation.scala	Mon Sep 05 22:09:52 2016 +0200
     7.3 @@ -105,8 +105,8 @@
     7.4                case XML.Elem(Markup(Markup.SENDBACK, props), b) =>
     7.5                  val props1 =
     7.6                    props.map({
     7.7 -                    case (Markup.ID, Properties.Value.Long(id)) if id == state0.exec_id =>
     7.8 -                      (Markup.ID, Properties.Value.Long(command.id))
     7.9 +                    case (Markup.ID, Value.Long(id)) if id == state0.exec_id =>
    7.10 +                      (Markup.ID, Value.Long(command.id))
    7.11                      case p => p
    7.12                    })
    7.13                  XML.Elem(Markup(Markup.SENDBACK, props1), resolve(b))
     8.1 --- a/src/Pure/System/bash.scala	Mon Sep 05 21:09:50 2016 +0200
     8.2 +++ b/src/Pure/System/bash.scala	Mon Sep 05 22:09:52 2016 +0200
     8.3 @@ -124,7 +124,7 @@
     8.4            if (timing_file.isFile) {
     8.5              val t =
     8.6                Word.explode(File.read(timing_file)) match {
     8.7 -                case List(Properties.Value.Long(elapsed), Properties.Value.Long(cpu)) =>
     8.8 +                case List(Value.Long(elapsed), Value.Long(cpu)) =>
     8.9                    Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero)
    8.10                  case _ => Timing.zero
    8.11                }
     9.1 --- a/src/Pure/System/options.scala	Mon Sep 05 21:09:50 2016 +0200
     9.2 +++ b/src/Pure/System/options.scala	Mon Sep 05 22:09:52 2016 +0200
     9.3 @@ -250,25 +250,25 @@
     9.4  
     9.5    class Bool_Access
     9.6    {
     9.7 -    def apply(name: String): Boolean = get(name, Options.Bool, Properties.Value.Boolean.unapply)
     9.8 +    def apply(name: String): Boolean = get(name, Options.Bool, Value.Boolean.unapply)
     9.9      def update(name: String, x: Boolean): Options =
    9.10 -      put(name, Options.Bool, Properties.Value.Boolean(x))
    9.11 +      put(name, Options.Bool, Value.Boolean(x))
    9.12    }
    9.13    val bool = new Bool_Access
    9.14  
    9.15    class Int_Access
    9.16    {
    9.17 -    def apply(name: String): Int = get(name, Options.Int, Properties.Value.Int.unapply)
    9.18 +    def apply(name: String): Int = get(name, Options.Int, Value.Int.unapply)
    9.19      def update(name: String, x: Int): Options =
    9.20 -      put(name, Options.Int, Properties.Value.Int(x))
    9.21 +      put(name, Options.Int, Value.Int(x))
    9.22    }
    9.23    val int = new Int_Access
    9.24  
    9.25    class Real_Access
    9.26    {
    9.27 -    def apply(name: String): Double = get(name, Options.Real, Properties.Value.Double.unapply)
    9.28 +    def apply(name: String): Double = get(name, Options.Real, Value.Double.unapply)
    9.29      def update(name: String, x: Double): Options =
    9.30 -      put(name, Options.Real, Properties.Value.Double(x))
    9.31 +      put(name, Options.Real, Value.Double(x))
    9.32    }
    9.33    val real = new Real_Access
    9.34  
    10.1 --- a/src/Pure/Tools/build.scala	Mon Sep 05 21:09:50 2016 +0200
    10.2 +++ b/src/Pure/Tools/build.scala	Mon Sep 05 22:09:52 2016 +0200
    10.3 @@ -790,7 +790,7 @@
    10.4        "c" -> (_ => clean_build = true),
    10.5        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
    10.6        "g:" -> (arg => session_groups = session_groups ::: List(arg)),
    10.7 -      "j:" -> (arg => max_jobs = Properties.Value.Int.parse(arg)),
    10.8 +      "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
    10.9        "k:" -> (arg => check_keywords = check_keywords + arg),
   10.10        "l" -> (_ => list_files = true),
   10.11        "n" -> (_ => no_build = true),
    11.1 --- a/src/Pure/Tools/build_doc.scala	Mon Sep 05 21:09:50 2016 +0200
    11.2 +++ b/src/Pure/Tools/build_doc.scala	Mon Sep 05 22:09:52 2016 +0200
    11.3 @@ -88,7 +88,7 @@
    11.4    suitable document_variants entry.
    11.5  """,
    11.6        "a" -> (_ => all_docs = true),
    11.7 -      "j:" -> (arg => max_jobs = Properties.Value.Int.parse(arg)),
    11.8 +      "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
    11.9        "s" -> (_ => system_mode = true))
   11.10  
   11.11      val docs = getopts(args)
    12.1 --- a/src/Pure/Tools/build_stats.scala	Mon Sep 05 21:09:50 2016 +0200
    12.2 +++ b/src/Pure/Tools/build_stats.scala	Mon Sep 05 22:09:52 2016 +0200
    12.3 @@ -38,8 +38,6 @@
    12.4  
    12.5    def parse(text: String): Build_Stats =
    12.6    {
    12.7 -    import Properties.Value
    12.8 -
    12.9      val ml_options = new mutable.ListBuffer[(String, String)]
   12.10      var finished = Map.empty[String, Timing]
   12.11      var timing = Map.empty[String, Timing]
   12.12 @@ -208,11 +206,11 @@
   12.13          "D:" -> (arg => target_dir = Path.explode(arg)),
   12.14          "M" -> (_ => ml_timing = Some(true)),
   12.15          "S:" -> (arg => only_sessions = space_explode(',', arg).toSet),
   12.16 -        "T:" -> (arg => elapsed_threshold = Time.minutes(Properties.Value.Double.parse(arg))),
   12.17 -        "l:" -> (arg => history_length = Properties.Value.Int.parse(arg)),
   12.18 +        "T:" -> (arg => elapsed_threshold = Time.minutes(Value.Double.parse(arg))),
   12.19 +        "l:" -> (arg => history_length = Value.Int.parse(arg)),
   12.20          "m" -> (_ => ml_timing = Some(false)),
   12.21          "s:" -> (arg =>
   12.22 -          space_explode('x', arg).map(Properties.Value.Int.parse(_)) match {
   12.23 +          space_explode('x', arg).map(Value.Int.parse(_)) match {
   12.24              case List(w, h) if w > 0 && h > 0 => size = (w, h)
   12.25              case _ => error("Error bad PNG image size: " + quote(arg))
   12.26            }))
    13.1 --- a/src/Pure/Tools/debugger.scala	Mon Sep 05 21:09:50 2016 +0200
    13.2 +++ b/src/Pure/Tools/debugger.scala	Mon Sep 05 22:09:52 2016 +0200
    13.3 @@ -234,8 +234,8 @@
    13.4          "Debugger.breakpoint",
    13.5          Symbol.encode(command.node_name.node),
    13.6          Document_ID(command.id),
    13.7 -        Properties.Value.Long(breakpoint),
    13.8 -        Properties.Value.Boolean(breakpoint_state))
    13.9 +        Value.Long(breakpoint),
   13.10 +        Value.Boolean(breakpoint_state))
   13.11        state1
   13.12      })
   13.13    }
    14.1 --- a/src/Pure/Tools/simplifier_trace.scala	Mon Sep 05 21:09:50 2016 +0200
    14.2 +++ b/src/Pure/Tools/simplifier_trace.scala	Mon Sep 05 22:09:52 2016 +0200
    14.3 @@ -165,7 +165,7 @@
    14.4      def do_reply(session: Session, serial: Long, answer: Answer)
    14.5      {
    14.6        session.protocol_command(
    14.7 -        "Simplifier_Trace.reply", Properties.Value.Long(serial), answer.name)
    14.8 +        "Simplifier_Trace.reply", Value.Long(serial), answer.name)
    14.9      }
   14.10  
   14.11      Consumer_Thread.fork[Any]("Simplifier_Trace.manager", daemon = true)(
    15.1 --- a/src/Pure/build-jars	Mon Sep 05 21:09:50 2016 +0200
    15.2 +++ b/src/Pure/build-jars	Mon Sep 05 22:09:52 2016 +0200
    15.3 @@ -50,6 +50,7 @@
    15.4    General/timing.scala
    15.5    General/untyped.scala
    15.6    General/url.scala
    15.7 +  General/value.scala
    15.8    General/word.scala
    15.9    General/xz_file.scala
   15.10    Isar/document_structure.scala
    16.1 --- a/src/Tools/jEdit/src/monitor_dockable.scala	Mon Sep 05 21:09:50 2016 +0200
    16.2 +++ b/src/Tools/jEdit/src/monitor_dockable.scala	Mon Sep 05 22:09:52 2016 +0200
    16.3 @@ -33,7 +33,7 @@
    16.4      statistics = statistics.enqueue(stats)
    16.5      statistics_length += 1
    16.6      limit_data.text match {
    16.7 -      case Properties.Value.Int(limit) =>
    16.8 +      case Value.Int(limit) =>
    16.9          while (statistics_length > limit) {
   16.10            statistics = statistics.dequeue._2
   16.11            statistics_length -= 1
   16.12 @@ -91,7 +91,7 @@
   16.13    private val limit_data = new TextField("200", 5) {
   16.14      tooltip = "Limit for accumulated data"
   16.15      verifier = (s: String) =>
   16.16 -      s match { case Properties.Value.Int(x) => x > 0 case _ => false }
   16.17 +      s match { case Value.Int(x) => x > 0 case _ => false }
   16.18      reactions += { case ValueChanged(_) => input_delay.invoke() }
   16.19    }
   16.20  
    17.1 --- a/src/Tools/jEdit/src/query_dockable.scala	Mon Sep 05 21:09:50 2016 +0200
    17.2 +++ b/src/Tools/jEdit/src/query_dockable.scala	Mon Sep 05 22:09:52 2016 +0200
    17.3 @@ -102,7 +102,7 @@
    17.4      private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
    17.5        tooltip = "Limit of displayed results"
    17.6        verifier = (s: String) =>
    17.7 -        s match { case Properties.Value.Int(x) => x >= 0 case _ => false }
    17.8 +        s match { case Value.Int(x) => x >= 0 case _ => false }
    17.9        listenTo(keys)
   17.10        reactions += { case KeyPressed(_, Key.Enter, 0, _) => apply_query() }
   17.11      }
    18.1 --- a/src/Tools/jEdit/src/timing_dockable.scala	Mon Sep 05 21:09:50 2016 +0200
    18.2 +++ b/src/Tools/jEdit/src/timing_dockable.scala	Mon Sep 05 22:09:52 2016 +0200
    18.3 @@ -132,14 +132,14 @@
    18.4      reactions += {
    18.5        case _: ValueChanged =>
    18.6          text match {
    18.7 -          case Properties.Value.Double(x) if x >= 0.0 => timing_threshold = x
    18.8 +          case Value.Double(x) if x >= 0.0 => timing_threshold = x
    18.9            case _ =>
   18.10          }
   18.11          handle_update()
   18.12      }
   18.13      tooltip = threshold_tooltip
   18.14      verifier = ((s: String) =>
   18.15 -      s match { case Properties.Value.Double(x) => x >= 0.0 case _ => false })
   18.16 +      s match { case Value.Double(x) => x >= 0.0 case _ => false })
   18.17    }
   18.18  
   18.19    private val controls =