95 def script_file(path: Path): XML.Elem = script_file(Url.print_file(path.file)) |
95 def script_file(path: Path): XML.Elem = script_file(Url.print_file(path.file)) |
96 |
96 |
97 |
97 |
98 /* output text with control symbols */ |
98 /* output text with control symbols */ |
99 |
99 |
100 private val control = |
100 private val control: Map[Symbol.Symbol, Operator] = |
101 Map( |
101 Map( |
102 Symbol.sub -> sub, Symbol.sub_decoded -> sub, |
102 Symbol.sub -> sub, Symbol.sub_decoded -> sub, |
103 Symbol.sup -> sup, Symbol.sup_decoded -> sup, |
103 Symbol.sup -> sup, Symbol.sup_decoded -> sup, |
104 Symbol.bold -> bold, Symbol.bold_decoded -> bold) |
104 Symbol.bold -> bold, Symbol.bold_decoded -> bold) |
105 |
105 |
106 private val control_block_begin = |
106 private val control_block_begin: Map[Symbol.Symbol, Operator] = |
107 Map( |
107 Map( |
108 Symbol.bsub -> sub, Symbol.bsub_decoded -> sub, |
108 Symbol.bsub -> sub, Symbol.bsub_decoded -> sub, |
109 Symbol.bsup -> sup, Symbol.bsup_decoded -> sup) |
109 Symbol.bsup -> sup, Symbol.bsup_decoded -> sup) |
110 |
110 |
111 private val control_block_end = |
111 private val control_block_end: Map[Symbol.Symbol, Operator] = |
112 Map( |
112 Map( |
113 Symbol.esub -> sub, Symbol.esub_decoded -> sub, |
113 Symbol.esub -> sub, Symbol.esub_decoded -> sub, |
114 Symbol.esup -> sup, Symbol.esup_decoded -> sup) |
114 Symbol.esup -> sup, Symbol.esup_decoded -> sup) |
115 |
115 |
116 def is_control(sym: Symbol.Symbol): Boolean = control.isDefinedAt(sym) |
116 def is_control(sym: Symbol.Symbol): Boolean = control.isDefinedAt(sym) |