# HG changeset patch
# User wenzelm
# Date 1480874035 -3600
# Node ID 693389d87139e02fd5e8c43f2c39cd810dc0f4dd
# Parent  ff59fe6b6f6ae6041946fae9228633e8ed1c7e1d# Parent  e61de633a3eddc6f5baa123879e4c0eec05d41c8
merged

diff -r ff59fe6b6f6a -r 693389d87139 src/Tools/jEdit/src/isabelle.scala
--- 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)
             }
diff -r ff59fe6b6f6a -r 693389d87139 src/Tools/jEdit/src/text_structure.scala
--- 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)