src/Pure/Syntax/ast.ML
changeset 62663 bea354f6ff21
parent 56438 7f6b2634d853
child 62819 d3ff367a16a0
equal deleted inserted replaced
62662:291cc01f56f5 62663:bea354f6ff21
    64   | pretty_ast (Appl asts) = Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
    64   | pretty_ast (Appl asts) = Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
    65 
    65 
    66 fun pretty_rule (lhs, rhs) =
    66 fun pretty_rule (lhs, rhs) =
    67   Pretty.block [pretty_ast lhs, Pretty.str "  ->", Pretty.brk 2, pretty_ast rhs];
    67   Pretty.block [pretty_ast lhs, Pretty.str "  ->", Pretty.brk 2, pretty_ast rhs];
    68 
    68 
       
    69 val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty_ast);
       
    70 
    69 
    71 
    70 (* strip_positions *)
    72 (* strip_positions *)
    71 
    73 
    72 fun strip_positions (Appl ((t as Constant c) :: u :: (v as Variable x) :: asts)) =
    74 fun strip_positions (Appl ((t as Constant c) :: u :: (v as Variable x) :: asts)) =
    73       if member (op =) Term_Position.markers c andalso is_some (Term_Position.decode x)
    75       if member (op =) Term_Position.markers c andalso is_some (Term_Position.decode x)