--- a/src/Tools/jEdit/src/isabelle.scala Tue Nov 29 16:58:10 2016 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Sun Dec 04 18:53:55 2016 +0100
@@ -277,7 +277,7 @@
: (List[Token], Scan.Line_Context) =
{
val text = JEdit_Lib.try_get_text(buffer, Text.Range(start, stop)).getOrElse("")
- val (toks, context1) = Token.explode_line(syntax.keywords, text, context)
+ val (toks, context1) = Token.explode_line(keywords, text, context)
val toks1 = toks.filterNot(_.is_space)
(toks1, context1)
}
--- a/src/Tools/jEdit/src/text_structure.scala Tue Nov 29 16:58:10 2016 +0100
+++ b/src/Tools/jEdit/src/text_structure.scala Sun Dec 04 18:53:55 2016 +0100
@@ -142,7 +142,6 @@
val indent =
if (Token_Markup.Line_Context.prev(buffer, current_line).get_context == Scan.Finished) {
line_head(current_line) match {
- case None => indent_structure + indent_brackets + indent_extra
case Some(info @ Text.Info(range, tok)) =>
if (tok.is_begin ||
keywords.is_before_command(tok) ||
@@ -166,7 +165,16 @@
indent_structure + indent_brackets + indent_size - indent_offset(tok) -
indent_offset(prev_tok) - indent_indent(prev_tok)
}
- }
+ }
+ case None =>
+ prev_line_command match {
+ case None =>
+ val extra = if (head_is_quasi_command(prev_line)) indent_extra else 0
+ line_indent(prev_line) + indent_brackets + extra
+ case Some(prev_tok) =>
+ indent_structure + indent_brackets + indent_size -
+ indent_offset(prev_tok) - indent_indent(prev_tok)
+ }
}
}
else line_indent(current_line)