# HG changeset patch
# User wenzelm
# Date 869225715 -7200
# Node ID df4d0dad2b4e96e86c14dcb25f1477a059f4d230
# Parent  88edd3450460fdb70254de38c23a79322853e40a
tuned warning;
renamed |-> <-| <-> to Parse/PrintRule;

diff -r 88edd3450460 -r df4d0dad2b4e src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Jul 18 13:33:20 1997 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Jul 18 13:35:15 1997 +0200
@@ -5,8 +5,6 @@
 Root of Isabelle's syntax module.
 *)
 
-infix |-> <-| <->;
-
 signature BASIC_SYNTAX =
 sig
   include AST0
@@ -25,9 +23,9 @@
   include MIXFIX1
   include PRINTER0
   datatype 'a trrule =
-    |-> of 'a * 'a |
-    <-| of 'a * 'a |
-    <-> of 'a * 'a
+    ParseRule of 'a * 'a |
+    PrintRule of 'a * 'a |
+    ParsePrintRule of 'a * 'a
   type syntax
   val extend_log_types: syntax -> string list -> syntax
   val extend_type_gram: syntax -> (string * int * mixfix) list -> syntax
@@ -355,11 +353,11 @@
     val chars = SymbolFont.read_charnames (explode str);
     val pts = parse gram root' (tokenize lexicon xids chars);
 
-    fun show_pt pt = writeln (str_of_ast (pt_to_ast (K None) pt));
+    fun show_pt pt = warning (str_of_ast (pt_to_ast (K None) pt));
   in
     if length pts > ! ambiguity_level then
       (warning ("Ambiguous input " ^ quote str);
-       writeln "produces the following parse trees:";
+       warning "produces the following parse trees:";
        seq show_pt pts)
     else ();
     map (pt_to_ast (lookup_trtab parse_ast_trtab)) pts
@@ -395,21 +393,21 @@
 (** prepare translation rules **)
 
 datatype 'a trrule =
-  op |-> of 'a * 'a |
-  op <-| of 'a * 'a |
-  op <-> of 'a * 'a;
+  ParseRule of 'a * 'a |
+  PrintRule of 'a * 'a |
+  ParsePrintRule of 'a * 'a;
 
-fun map_rule f (x |-> y) = (f x |-> f y)
-  | map_rule f (x <-| y) = (f x <-| f y)
-  | map_rule f (x <-> y) = (f x <-> f y);
+fun map_rule f (ParseRule (x, y)) = ParseRule (f x, f y)
+  | map_rule f (PrintRule (x, y)) = PrintRule (f x, f y)
+  | map_rule f (ParsePrintRule (x, y)) = ParsePrintRule (f x, f y);
 
-fun right_rule (pat1 |-> pat2) = Some (pat1, pat2)
-  | right_rule (pat1 <-| pat2) = None
-  | right_rule (pat1 <-> pat2) = Some (pat1, pat2);
+fun parse_rule (ParseRule pats) = Some pats
+  | parse_rule (PrintRule _) = None
+  | parse_rule (ParsePrintRule pats) = Some pats;
 
-fun left_rule (pat1 |-> pat2) = None
-  | left_rule (pat1 <-| pat2) = Some (pat2, pat1)
-  | left_rule (pat1 <-> pat2) = Some (pat2, pat1);
+fun print_rule (ParseRule _) = None
+  | print_rule (PrintRule pats) = Some (swap pats)
+  | print_rule (ParsePrintRule pats) = Some (swap pats);
 
 
 fun check_rule (rule as (lhs, rhs)) =
@@ -439,8 +437,8 @@
 
 fun prep_rules rd_pat raw_rules =
   let val rules = map (map_rule rd_pat) raw_rules in
-    (map check_rule (mapfilter right_rule rules),
-      map check_rule (mapfilter left_rule rules))
+    (map check_rule (mapfilter parse_rule rules),
+      map check_rule (mapfilter print_rule rules))
   end