equal
deleted
inserted
replaced
1 (* Title: Pure/General/symbol_pos.ML |
1 (* Title: Pure/General/symbol_pos.ML |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Symbols with explicit position information. |
4 Symbols with explicit position information. |
5 *) |
5 *) |
6 |
|
7 val legacy_isub_isup = Unsynchronized.ref false; |
|
8 |
6 |
9 signature SYMBOL_POS = |
7 signature SYMBOL_POS = |
10 sig |
8 sig |
11 type T = Symbol.symbol * Position.T |
9 type T = Symbol.symbol * Position.T |
12 val symbol: T -> Symbol.symbol |
10 val symbol: T -> Symbol.symbol |