1.1 --- a/src/Pure/IsaMakefile	Tue Jul 12 15:12:50 2011 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Tue Jul 12 15:17:37 2011 +0200
     1.3 @@ -130,7 +130,6 @@
     1.4    Isar/overloading.ML					\
     1.5    Isar/parse.ML						\
     1.6    Isar/parse_spec.ML					\
     1.7 -  Isar/parse_value.ML					\
     1.8    Isar/proof.ML						\
     1.9    Isar/proof_context.ML					\
    1.10    Isar/proof_display.ML					\

     2.1 --- a/src/Pure/Isar/parse_value.ML	Tue Jul 12 15:12:50 2011 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,42 +0,0 @@
     2.4 -(*  Title:      Pure/Isar/parse_value.ML
     2.5 -    Author:     Makarius
     2.6 -
     2.7 -Outer syntax parsers for basic ML values.
     2.8 -*)
     2.9 -
    2.10 -signature PARSE_VALUE =
    2.11 -sig
    2.12 -  val comma: 'a parser -> 'a parser
    2.13 -  val equal: 'a parser -> 'a parser
    2.14 -  val parens: 'a parser -> 'a parser
    2.15 -  val unit: unit parser
    2.16 -  val pair: 'a parser -> 'b parser -> ('a * 'b) parser
    2.17 -  val triple: 'a parser -> 'b parser -> 'c parser -> ('a * 'b * 'c) parser
    2.18 -  val list: 'a parser -> 'a list parser
    2.19 -  val properties: Properties.T parser
    2.20 -end;
    2.21 -
    2.22 -structure Parse_Value: PARSE_VALUE =
    2.23 -struct
    2.24 -
    2.25 -(* syntax utilities *)
    2.26 -
    2.27 -fun comma p = Parse.$$$ "," |-- Parse.!!! p;
    2.28 -fun equal p = Parse.$$$ "=" |-- Parse.!!! p;
    2.29 -fun parens p = Parse.$$$ "(" |-- Parse.!!! (p --| Parse.$$$ ")");
    2.30 -
    2.31 -
    2.32 -(* tuples *)
    2.33 -
    2.34 -val unit = parens (Scan.succeed ());
    2.35 -fun pair p1 p2 = parens (p1 -- comma p2);
    2.36 -fun triple p1 p2 p3 = parens (p1 -- comma p2 -- comma p3) >> Parse.triple1;
    2.37 -
    2.38 -
    2.39 -(* lists *)
    2.40 -
    2.41 -fun list p = parens (Parse.enum "," p);
    2.42 -val properties = list (Parse.string -- equal Parse.string);
    2.43 -
    2.44 -end;
    2.45 -

     3.1 --- a/src/Pure/ROOT.ML	Tue Jul 12 15:12:50 2011 +0200
     3.2 +++ b/src/Pure/ROOT.ML	Tue Jul 12 15:17:37 2011 +0200
     3.3 @@ -188,7 +188,6 @@
     3.4  use "Isar/token.ML";
     3.5  use "Isar/keyword.ML";
     3.6  use "Isar/parse.ML";
     3.7 -use "Isar/parse_value.ML";
     3.8  use "Isar/args.ML";
     3.9  
    3.10  (*ML support*)

     4.1 --- a/src/Pure/System/isabelle_syntax.scala	Tue Jul 12 15:12:50 2011 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,74 +0,0 @@
     4.4 -/*  Title:      Pure/System/isabelle_syntax.scala
     4.5 -    Author:     Makarius
     4.6 -
     4.7 -Isabelle outer syntax.
     4.8 -*/
     4.9 -
    4.10 -package isabelle
    4.11 -
    4.12 -
    4.13 -object Isabelle_Syntax
    4.14 -{
    4.15 -  /* string token */
    4.16 -
    4.17 -  def append_string(str: String, result: StringBuilder)
    4.18 -  {
    4.19 -    result.append("\"")
    4.20 -    for (c <- str) {
    4.21 -      if ((c < 32 && c != 5 && c != 6) || c == '\\' || c == '\"') {
    4.22 -        result.append("\\0")
    4.23 -        if (c < 10) result.append('0')
    4.24 -        if (c < 100) result.append('0')
    4.25 -        result.append(c.asInstanceOf[Int].toString)
    4.26 -      }
    4.27 -      else result.append(c)
    4.28 -    }
    4.29 -    result.append("\"")
    4.30 -  }
    4.31 -
    4.32 -  def encode_string(str: String) =
    4.33 -  {
    4.34 -    val result = new StringBuilder(str.length + 10)
    4.35 -    append_string(str, result)
    4.36 -    result.toString
    4.37 -  }
    4.38 -
    4.39 -
    4.40 -  /* list */
    4.41 -
    4.42 -  def append_list[A](append_elem: (A, StringBuilder) => Unit, body: Iterable[A],
    4.43 -    result: StringBuilder)
    4.44 -  {
    4.45 -    result.append("(")
    4.46 -    val elems = body.iterator
    4.47 -    if (elems.hasNext) append_elem(elems.next, result)
    4.48 -    while (elems.hasNext) {
    4.49 -      result.append(", ")
    4.50 -      append_elem(elems.next, result)
    4.51 -    }
    4.52 -    result.append(")")
    4.53 -  }
    4.54 -
    4.55 -  def encode_list[A](append_elem: (A, StringBuilder) => Unit, elems: Iterable[A]) =
    4.56 -  {
    4.57 -    val result = new StringBuilder
    4.58 -    append_list(append_elem, elems, result)
    4.59 -    result.toString
    4.60 -  }
    4.61 -
    4.62 -
    4.63 -  /* properties */
    4.64 -
    4.65 -  def append_properties(props: List[(String, String)], result: StringBuilder)
    4.66 -  {
    4.67 -    append_list((p: (String, String), res) =>
    4.68 -      { append_string(p._1, res); res.append(" = "); append_string(p._2, res) }, props, result)
    4.69 -  }
    4.70 -
    4.71 -  def encode_properties(props: List[(String, String)]) =
    4.72 -  {
    4.73 -    val result = new StringBuilder
    4.74 -    append_properties(props, result)
    4.75 -    result.toString
    4.76 -  }
    4.77 -}

     5.1 --- a/src/Pure/build-jars	Tue Jul 12 15:12:50 2011 +0200
     5.2 +++ b/src/Pure/build-jars	Tue Jul 12 15:17:37 2011 +0200
     5.3 @@ -42,7 +42,6 @@
     5.4    System/invoke_scala.scala
     5.5    System/isabelle_charset.scala
     5.6    System/isabelle_process.scala
     5.7 -  System/isabelle_syntax.scala
     5.8    System/isabelle_system.scala
     5.9    System/platform.scala
    5.10    System/session.scala