# HG changeset patch
# User wenzelm
# Date 1310476657 -7200
# Node ID 6dd13e111d308d03ab2ce9cab41679684f919c39
# Parent  b361c7d184e7bfa7dd1edb89c5192088c88c7919
discontinued obsolete Isabelle_Syntax and Parse_Value -- superseded by Outer_Syntax.quote_string and XML.Encode, Term_XML.Encode etc.;

diff -r b361c7d184e7 -r 6dd13e111d30 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Tue Jul 12 15:12:50 2011 +0200
+++ b/src/Pure/IsaMakefile	Tue Jul 12 15:17:37 2011 +0200
@@ -130,7 +130,6 @@
   Isar/overloading.ML					\
   Isar/parse.ML						\
   Isar/parse_spec.ML					\
-  Isar/parse_value.ML					\
   Isar/proof.ML						\
   Isar/proof_context.ML					\
   Isar/proof_display.ML					\
diff -r b361c7d184e7 -r 6dd13e111d30 src/Pure/Isar/parse_value.ML
--- a/src/Pure/Isar/parse_value.ML	Tue Jul 12 15:12:50 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-(*  Title:      Pure/Isar/parse_value.ML
-    Author:     Makarius
-
-Outer syntax parsers for basic ML values.
-*)
-
-signature PARSE_VALUE =
-sig
-  val comma: 'a parser -> 'a parser
-  val equal: 'a parser -> 'a parser
-  val parens: 'a parser -> 'a parser
-  val unit: unit parser
-  val pair: 'a parser -> 'b parser -> ('a * 'b) parser
-  val triple: 'a parser -> 'b parser -> 'c parser -> ('a * 'b * 'c) parser
-  val list: 'a parser -> 'a list parser
-  val properties: Properties.T parser
-end;
-
-structure Parse_Value: PARSE_VALUE =
-struct
-
-(* syntax utilities *)
-
-fun comma p = Parse.$$$ "," |-- Parse.!!! p;
-fun equal p = Parse.$$$ "=" |-- Parse.!!! p;
-fun parens p = Parse.$$$ "(" |-- Parse.!!! (p --| Parse.$$$ ")");
-
-
-(* tuples *)
-
-val unit = parens (Scan.succeed ());
-fun pair p1 p2 = parens (p1 -- comma p2);
-fun triple p1 p2 p3 = parens (p1 -- comma p2 -- comma p3) >> Parse.triple1;
-
-
-(* lists *)
-
-fun list p = parens (Parse.enum "," p);
-val properties = list (Parse.string -- equal Parse.string);
-
-end;
-
diff -r b361c7d184e7 -r 6dd13e111d30 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Jul 12 15:12:50 2011 +0200
+++ b/src/Pure/ROOT.ML	Tue Jul 12 15:17:37 2011 +0200
@@ -188,7 +188,6 @@
 use "Isar/token.ML";
 use "Isar/keyword.ML";
 use "Isar/parse.ML";
-use "Isar/parse_value.ML";
 use "Isar/args.ML";
 
 (*ML support*)
diff -r b361c7d184e7 -r 6dd13e111d30 src/Pure/System/isabelle_syntax.scala
--- a/src/Pure/System/isabelle_syntax.scala	Tue Jul 12 15:12:50 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,74 +0,0 @@
-/*  Title:      Pure/System/isabelle_syntax.scala
-    Author:     Makarius
-
-Isabelle outer syntax.
-*/
-
-package isabelle
-
-
-object Isabelle_Syntax
-{
-  /* string token */
-
-  def append_string(str: String, result: StringBuilder)
-  {
-    result.append("\"")
-    for (c <- str) {
-      if ((c < 32 && c != 5 && c != 6) || c == '\\' || c == '\"') {
-        result.append("\\0")
-        if (c < 10) result.append('0')
-        if (c < 100) result.append('0')
-        result.append(c.asInstanceOf[Int].toString)
-      }
-      else result.append(c)
-    }
-    result.append("\"")
-  }
-
-  def encode_string(str: String) =
-  {
-    val result = new StringBuilder(str.length + 10)
-    append_string(str, result)
-    result.toString
-  }
-
-
-  /* list */
-
-  def append_list[A](append_elem: (A, StringBuilder) => Unit, body: Iterable[A],
-    result: StringBuilder)
-  {
-    result.append("(")
-    val elems = body.iterator
-    if (elems.hasNext) append_elem(elems.next, result)
-    while (elems.hasNext) {
-      result.append(", ")
-      append_elem(elems.next, result)
-    }
-    result.append(")")
-  }
-
-  def encode_list[A](append_elem: (A, StringBuilder) => Unit, elems: Iterable[A]) =
-  {
-    val result = new StringBuilder
-    append_list(append_elem, elems, result)
-    result.toString
-  }
-
-
-  /* properties */
-
-  def append_properties(props: List[(String, String)], result: StringBuilder)
-  {
-    append_list((p: (String, String), res) =>
-      { append_string(p._1, res); res.append(" = "); append_string(p._2, res) }, props, result)
-  }
-
-  def encode_properties(props: List[(String, String)]) =
-  {
-    val result = new StringBuilder
-    append_properties(props, result)
-    result.toString
-  }
-}
diff -r b361c7d184e7 -r 6dd13e111d30 src/Pure/build-jars
--- a/src/Pure/build-jars	Tue Jul 12 15:12:50 2011 +0200
+++ b/src/Pure/build-jars	Tue Jul 12 15:17:37 2011 +0200
@@ -42,7 +42,6 @@
   System/invoke_scala.scala
   System/isabelle_charset.scala
   System/isabelle_process.scala
-  System/isabelle_syntax.scala
   System/isabelle_system.scala
   System/platform.scala
   System/session.scala