src/Tools/jEdit/src/text_structure.scala
changeset 63442 f6b5124b7023
parent 63440 2ce032a41a3a
child 63445 5761bb8592dc
equal deleted inserted replaced
63441:4c3fa4dba79f 63442:f6b5124b7023
   107 
   107 
   108           val indent =
   108           val indent =
   109             head_token(current_line) match {
   109             head_token(current_line) match {
   110               case None => indent_structure + indent_extra
   110               case None => indent_structure + indent_extra
   111               case Some(tok) =>
   111               case Some(tok) =>
   112                 if (keywords.is_command(tok, Keyword.theory)) indent_begin
   112                 if (keywords.is_before_command(tok) ||
       
   113                     keywords.is_command(tok, Keyword.theory)) indent_begin
   113                 else if (tok.is_command) indent_structure + indent_begin - indent_offset(tok)
   114                 else if (tok.is_command) indent_structure + indent_begin - indent_offset(tok)
   114                 else {
   115                 else {
   115                   prev_command match {
   116                   prev_command match {
   116                     case None =>
   117                     case None =>
   117                       val extra =
   118                       val extra =