32 |
32 |
33 (* parse trees *) |
33 (* parse trees *) |
34 |
34 |
35 fun report_parse_tree depth space = |
35 fun report_parse_tree depth space = |
36 let |
36 let |
37 val report_text = |
37 val reported_text = |
38 (case Context.thread_data () of |
38 (case Context.thread_data () of |
39 SOME (Context.Proof ctxt) => Context_Position.report_text ctxt |
39 SOME (Context.Proof ctxt) => Context_Position.reported_text ctxt |
40 | _ => Position.report_text); |
40 | _ => Position.reported_text); |
41 |
41 |
42 fun report_entity kind loc decl = |
42 fun reported_entity kind loc decl = |
43 report_text (position_of loc) |
43 reported_text (position_of loc) |
44 (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) ""; |
44 (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) ""; |
45 |
45 |
46 fun report loc (PolyML.PTtype types) = |
46 fun reported loc (PolyML.PTtype types) = |
47 cons (fn () => |
47 cons |
48 PolyML.NameSpace.displayTypeExpression (types, depth, space) |
48 (PolyML.NameSpace.displayTypeExpression (types, depth, space) |
49 |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |
49 |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |
50 |> report_text (position_of loc) Markup.ML_typing) |
50 |> reported_text (position_of loc) Markup.ML_typing) |
51 | report loc (PolyML.PTdeclaredAt decl) = |
51 | reported loc (PolyML.PTdeclaredAt decl) = |
52 cons (fn () => report_entity Markup.ML_defN loc decl) |
52 cons (reported_entity Markup.ML_defN loc decl) |
53 | report loc (PolyML.PTopenedAt decl) = |
53 | reported loc (PolyML.PTopenedAt decl) = |
54 cons (fn () => report_entity Markup.ML_openN loc decl) |
54 cons (reported_entity Markup.ML_openN loc decl) |
55 | report loc (PolyML.PTstructureAt decl) = |
55 | reported loc (PolyML.PTstructureAt decl) = |
56 cons (fn () => report_entity Markup.ML_structN loc decl) |
56 cons (reported_entity Markup.ML_structN loc decl) |
57 | report _ (PolyML.PTnextSibling tree) = report_tree (tree ()) |
57 | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ()) |
58 | report _ (PolyML.PTfirstChild tree) = report_tree (tree ()) |
58 | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ()) |
59 | report _ _ = I |
59 | reported _ _ = I |
60 and report_tree (loc, props) = fold (report loc) props; |
60 and reported_tree (loc, props) = fold (reported loc) props; |
61 in fn tree => List.app (fn e => e ()) (report_tree tree []) end; |
61 in fn tree => Output.report (implode (reported_tree tree [])) end; |
62 |
62 |
63 |
63 |
64 (* eval ML source tokens *) |
64 (* eval ML source tokens *) |
65 |
65 |
66 fun eval verbose pos toks = |
66 fun eval verbose pos toks = |