| changeset 62512 | 922e702ae8ca |
| parent 62500 | ff99681b3fd8 |
| parent 62511 | 93fa1efc7219 |
| child 62513 | 702085ca8564 |
| 62500:ff99681b3fd8 | 62512:922e702ae8ca |
|---|---|
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; |