discontinued obsolete Isabelle_Syntax and Parse_Value -- superseded by Outer_Syntax.quote_string and XML.Encode, Term_XML.Encode etc.;
--- 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 \
--- 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;
-
--- 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*)
--- 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
- }
-}
--- 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