src/Tools/jEdit/src/isabelle.scala
changeset 63477 f5c81436b930
parent 63455 019856db2bb6
child 63484 2033a3960c36
equal deleted inserted replaced
63476:ff1d86b07751 63477:f5c81436b930
   280 
   280 
   281             val context0 = Token_Markup.Line_Context.prev(buffer, line).get_context
   281             val context0 = Token_Markup.Line_Context.prev(buffer, line).get_context
   282             val (tokens1, context1) = line_content(line_range.start, caret, context0)
   282             val (tokens1, context1) = line_content(line_range.start, caret, context0)
   283             val (tokens2, _) = line_content(caret, line_range.stop, context1)
   283             val (tokens2, _) = line_content(caret, line_range.stop, context1)
   284 
   284 
   285             if (tokens1.nonEmpty && tokens1.head.is_command) buffer.indentLine(line, true)
   285             if (tokens1.nonEmpty && tokens1.head.is_begin_or_command)
   286 
   286               buffer.indentLine(line, true)
   287             if (tokens2.isEmpty || tokens2.head.is_command)
   287 
       
   288             if (tokens2.isEmpty || tokens2.head.is_begin_or_command)
   288               JEdit_Lib.buffer_edit(buffer) {
   289               JEdit_Lib.buffer_edit(buffer) {
   289                 text_area.setSelectedText("\n")
   290                 text_area.setSelectedText("\n")
   290                 if (!buffer.indentLine(line + 1, true)) text_area.goToStartOfWhiteSpace(false)
   291                 if (!buffer.indentLine(line + 1, true)) text_area.goToStartOfWhiteSpace(false)
   291               }
   292               }
   292             else nl
   293             else nl