| changeset 62501 | 98fa1f9a292f |
| parent 62498 | 5dfcc9697f29 |
| child 62502 | 8857237c3a90 |
| 62498:5dfcc9697f29 | 62501:98fa1f9a292f |
|---|---|
1 (* Title: Pure/RAW/ml_parse_tree.ML |
|
2 Author: Makarius |
|
3 |
|
4 Additional ML parse tree components for Poly/ML. |
|
5 *) |
|
6 |
|
7 signature ML_PARSE_TREE = |
|
8 sig |
|
9 val completions: PolyML.ptProperties -> string list option |
|
10 val breakpoint: PolyML.ptProperties -> bool Unsynchronized.ref option |
|
11 end; |
|
12 |
|
13 structure ML_Parse_Tree: ML_PARSE_TREE = |
|
14 struct |
|
15 |
|
16 fun completions _ = NONE; |
|
17 fun breakpoint _ = NONE; |
|
18 |
|
19 end; |