# HG changeset patch # User wenzelm # Date 850219252 -3600 # Node ID 38295260a740cf66659672a0db5ff4b57bf4a54d # Parent 821f44a0abbae4a59bb3c2400e80a2277e000779 added chartrans_of; diff -r 821f44a0abba -r 38295260a740 src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Tue Dec 10 12:56:33 1996 +0100 +++ b/src/Pure/Syntax/printer.ML Tue Dec 10 13:00:52 1996 +0100 @@ -28,9 +28,10 @@ -> (string -> (Ast.ast list -> Ast.ast) option) -> Ast.ast -> Pretty.T val pretty_typ_ast: bool -> prtabs -> (string -> (Ast.ast list -> Ast.ast) option) -> Ast.ast -> Pretty.T + val chartrans_of: prtabs -> (string * string) list end; -structure Printer : PRINTER = +structure Printer: PRINTER = struct open Lexicon Ast SynExt TypeExt SynTrans; @@ -131,7 +132,7 @@ type prtabs = (string * ((symb list * int * int) list) Symtab.table) list; -fun prmodes_of l = filter_out (equal "") (map fst l); +fun prmodes_of prtabs = filter_out (equal "") (map fst prtabs); (*find tab for mode*) fun get_tab prtabs mode = @@ -151,19 +152,16 @@ fun xprod_to_fmt (XProd (_, _, "", _)) = None | xprod_to_fmt (XProd (_, xsymbs, const, pri)) = let - fun cons_str s (String s' :: syms) = String (s ^ s') :: syms - | cons_str s syms = String s :: syms; - fun arg (s, p) = (if s = "type" then TypArg else Arg) (if is_terminal s then max_pri else p); fun xsyms_to_syms (Delim s :: xsyms) = - apfst (cons_str s) (xsyms_to_syms xsyms) + apfst (cons (String s)) (xsyms_to_syms xsyms) | xsyms_to_syms (Argument s_p :: xsyms) = apfst (cons (arg s_p)) (xsyms_to_syms xsyms) | xsyms_to_syms (Space s :: xsyms) = - apfst (cons_str s) (xsyms_to_syms xsyms) + apfst (cons (String s)) (xsyms_to_syms xsyms) | xsyms_to_syms (Bg i :: xsyms) = let val (bsyms, xsyms') = xsyms_to_syms xsyms; @@ -310,4 +308,56 @@ Pretty.blk (0, pretty (tabs_of prtabs (! print_mode)) trf true false ast 0); + +(** character translations - generated from "symbols" syntax **) + +(* match_symbs *) + +(*match with symbs pattern, ignoring spaces, breaks, blocks*) + +local + exception NO_MATCH; + + fun strip ((sym as Arg _) :: syms) = sym :: strip syms + | strip (TypArg p :: syms) = Arg p :: strip syms + | strip ((sym as String s) :: syms) = + if forall is_blank (explode s) then strip syms + else sym :: strip syms + | strip (Break _ :: syms) = strip syms + | strip (Block (_, bsyms) :: syms) = strip bsyms @ strip syms + | strip [] = []; + + fun match (Arg p :: syms) (Arg p' :: syms') tr = + if p = p' then match syms syms' tr + else raise NO_MATCH + | match (String s :: syms) (String s' :: syms') tr = + if s = s' then match syms syms' tr + else if size s = 1 then match syms syms' ((s, s') :: tr) + else raise NO_MATCH + | match [] [] tr = tr + | match _ _ _ = raise NO_MATCH; +in + fun match_symbs (syms, n, p) (syms', n', p') = + if n = n' andalso p = p' then + match (strip syms) (strip syms') [] handle NO_MATCH => [] + else [] end; + + +(* chartrans_of *) + +fun chartrans_of prtabs = + let + val def_tab = get_tab prtabs ""; + val sym_tab = get_tab prtabs "symbols"; + + fun trans_of (c, symb) = + flat (map (match_symbs symb) (Symtab.lookup_multi (def_tab, c))); + in + distinct (flat (map trans_of (Symtab.dest_multi sym_tab))) +(* FIXME Symtab.make tr handle Symtab.DUPS cs + => error ("Ambiguous printer syntax of symbols: " ^ commas cs) *) + end; + + +end;