equal
deleted
inserted
replaced
146 str "(" |-- pt --| str "&" -- pt --| str ")" >> RealArith.Branch) input |
146 str "(" |-- pt --| str "&" -- pt --| str ")" >> RealArith.Branch) input |
147 end |
147 end |
148 |
148 |
149 (* scanner *) |
149 (* scanner *) |
150 |
150 |
151 fun cert_to_pss_tree ctxt input_str = Symbol.scanner "bad certificate" (parse_cert_tree ctxt) |
151 fun cert_to_pss_tree ctxt input_str = |
152 (filter_out Symbol.is_blank (Symbol.explode input_str)) |
152 Symbol.scanner "Bad certificate" (parse_cert_tree ctxt) |
|
153 (filter_out Symbol.is_blank (Symbol.explode input_str)) |
153 |
154 |
154 end |
155 end |
155 |
156 |
156 |
|