25 |
25 |
26 in |
26 in |
27 |
27 |
28 val _ = |
28 val _ = |
29 Theory.setup |
29 Theory.setup |
30 (setup_trace_method @{binding print_fact} |
30 (setup_trace_method \<^binding>\<open>print_fact\<close> |
31 (Scan.lift (Scan.ahead Parse.not_eof) -- Attrib.thms) |
31 (Scan.lift (Scan.ahead Parse.not_eof) -- Attrib.thms) |
32 (fn ctxt => fn (tok, thms) => |
32 (fn ctxt => fn (tok, thms) => |
33 (* FIXME proper formatting!? *) |
33 (* FIXME proper formatting!? *) |
34 Token.unparse tok ^ ": " ^ commas (map (Thm.string_of_thm ctxt) thms)) #> |
34 Token.unparse tok ^ ": " ^ commas (map (Thm.string_of_thm ctxt) thms)) #> |
35 setup_trace_method @{binding print_term} |
35 setup_trace_method \<^binding>\<open>print_term\<close> |
36 (Scan.lift (Scan.ahead Parse.not_eof) -- Args.term) |
36 (Scan.lift (Scan.ahead Parse.not_eof) -- Args.term) |
37 (fn ctxt => fn (tok, t) => |
37 (fn ctxt => fn (tok, t) => |
38 (* FIXME proper formatting!? *) |
38 (* FIXME proper formatting!? *) |
39 Token.unparse tok ^ ": " ^ Syntax.string_of_term ctxt t) #> |
39 Token.unparse tok ^ ": " ^ Syntax.string_of_term ctxt t) #> |
40 setup_trace_method @{binding print_type} |
40 setup_trace_method \<^binding>\<open>print_type\<close> |
41 (Scan.lift (Scan.ahead Parse.not_eof) -- Args.typ) |
41 (Scan.lift (Scan.ahead Parse.not_eof) -- Args.typ) |
42 (fn ctxt => fn (tok, t) => |
42 (fn ctxt => fn (tok, t) => |
43 (* FIXME proper formatting!? *) |
43 (* FIXME proper formatting!? *) |
44 Token.unparse tok ^ ": " ^ Syntax.string_of_typ ctxt t)); |
44 Token.unparse tok ^ ": " ^ Syntax.string_of_typ ctxt t)); |
45 |
45 |