equal
deleted
inserted
replaced
176 |
176 |
177 val context1 = |
177 val context1 = |
178 { |
178 { |
179 val (styled_tokens, context1) = |
179 val (styled_tokens, context1) = |
180 if (line_ctxt.isDefined && Isabelle.session.is_ready) { |
180 if (line_ctxt.isDefined && Isabelle.session.is_ready) { |
181 val syntax = Isabelle.session.current_syntax() |
181 val syntax = Isabelle.session.recent_syntax() |
182 val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get) |
182 val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get) |
183 val styled_tokens = |
183 val styled_tokens = |
184 tokens.map(tok => (Isabelle_Rendering.token_markup(syntax, tok), tok)) |
184 tokens.map(tok => (Isabelle_Rendering.token_markup(syntax, tok), tok)) |
185 (styled_tokens, new Line_Context(Some(ctxt1))) |
185 (styled_tokens, new Line_Context(Some(ctxt1))) |
186 } |
186 } |