src/Tools/jEdit/src/text_structure.scala

             if (Token_Markup.Line_Context.before(buffer, current_line).get_context != Scan.Finished)
               line_indent(current_line)
             else if (Token_Markup.Line_Context.after(buffer, current_line).structure.blank) 0
             else {
               line_head(current_line) match {
-                case Some(info @ Text.Info(range, tok)) =>
+                case Some(info) =>
+                  val tok = info.info
                   if (tok.is_begin ||
                       keywords.is_before_command(tok) ||
                       keywords.is_command(tok, Keyword.theory)) 0
                   else if (keywords.is_command(tok, Keyword.proof_enclose))
                     indent_structure + script_indent(info) - indent_offset(tok)