tuned warning;
authorwenzelm
Fri Jul 18 13:35:15 1997 +0200 (1997-07-18)
changeset 3526df4d0dad2b4e
parent 3525 88edd3450460
child 3527 b894f4c13df5
tuned warning;
renamed |-> <-| <-> to Parse/PrintRule;
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Fri Jul 18 13:33:20 1997 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Jul 18 13:35:15 1997 +0200
     1.3 @@ -5,8 +5,6 @@
     1.4  Root of Isabelle's syntax module.
     1.5  *)
     1.6  
     1.7 -infix |-> <-| <->;
     1.8 -
     1.9  signature BASIC_SYNTAX =
    1.10  sig
    1.11    include AST0
    1.12 @@ -25,9 +23,9 @@
    1.13    include MIXFIX1
    1.14    include PRINTER0
    1.15    datatype 'a trrule =
    1.16 -    |-> of 'a * 'a |
    1.17 -    <-| of 'a * 'a |
    1.18 -    <-> of 'a * 'a
    1.19 +    ParseRule of 'a * 'a |
    1.20 +    PrintRule of 'a * 'a |
    1.21 +    ParsePrintRule of 'a * 'a
    1.22    type syntax
    1.23    val extend_log_types: syntax -> string list -> syntax
    1.24    val extend_type_gram: syntax -> (string * int * mixfix) list -> syntax
    1.25 @@ -355,11 +353,11 @@
    1.26      val chars = SymbolFont.read_charnames (explode str);
    1.27      val pts = parse gram root' (tokenize lexicon xids chars);
    1.28  
    1.29 -    fun show_pt pt = writeln (str_of_ast (pt_to_ast (K None) pt));
    1.30 +    fun show_pt pt = warning (str_of_ast (pt_to_ast (K None) pt));
    1.31    in
    1.32      if length pts > ! ambiguity_level then
    1.33        (warning ("Ambiguous input " ^ quote str);
    1.34 -       writeln "produces the following parse trees:";
    1.35 +       warning "produces the following parse trees:";
    1.36         seq show_pt pts)
    1.37      else ();
    1.38      map (pt_to_ast (lookup_trtab parse_ast_trtab)) pts
    1.39 @@ -395,21 +393,21 @@
    1.40  (** prepare translation rules **)
    1.41  
    1.42  datatype 'a trrule =
    1.43 -  op |-> of 'a * 'a |
    1.44 -  op <-| of 'a * 'a |
    1.45 -  op <-> of 'a * 'a;
    1.46 +  ParseRule of 'a * 'a |
    1.47 +  PrintRule of 'a * 'a |
    1.48 +  ParsePrintRule of 'a * 'a;
    1.49  
    1.50 -fun map_rule f (x |-> y) = (f x |-> f y)
    1.51 -  | map_rule f (x <-| y) = (f x <-| f y)
    1.52 -  | map_rule f (x <-> y) = (f x <-> f y);
    1.53 +fun map_rule f (ParseRule (x, y)) = ParseRule (f x, f y)
    1.54 +  | map_rule f (PrintRule (x, y)) = PrintRule (f x, f y)
    1.55 +  | map_rule f (ParsePrintRule (x, y)) = ParsePrintRule (f x, f y);
    1.56  
    1.57 -fun right_rule (pat1 |-> pat2) = Some (pat1, pat2)
    1.58 -  | right_rule (pat1 <-| pat2) = None
    1.59 -  | right_rule (pat1 <-> pat2) = Some (pat1, pat2);
    1.60 +fun parse_rule (ParseRule pats) = Some pats
    1.61 +  | parse_rule (PrintRule _) = None
    1.62 +  | parse_rule (ParsePrintRule pats) = Some pats;
    1.63  
    1.64 -fun left_rule (pat1 |-> pat2) = None
    1.65 -  | left_rule (pat1 <-| pat2) = Some (pat2, pat1)
    1.66 -  | left_rule (pat1 <-> pat2) = Some (pat2, pat1);
    1.67 +fun print_rule (ParseRule _) = None
    1.68 +  | print_rule (PrintRule pats) = Some (swap pats)
    1.69 +  | print_rule (ParsePrintRule pats) = Some (swap pats);
    1.70  
    1.71  
    1.72  fun check_rule (rule as (lhs, rhs)) =
    1.73 @@ -439,8 +437,8 @@
    1.74  
    1.75  fun prep_rules rd_pat raw_rules =
    1.76    let val rules = map (map_rule rd_pat) raw_rules in
    1.77 -    (map check_rule (mapfilter right_rule rules),
    1.78 -      map check_rule (mapfilter left_rule rules))
    1.79 +    (map check_rule (mapfilter parse_rule rules),
    1.80 +      map check_rule (mapfilter print_rule rules))
    1.81    end
    1.82  
    1.83