src/Tools/jEdit/src/token_markup.scala

   ParserRuleSet, ModeProvider, XModeHandler}
 import org.gjt.sp.jedit.indent.IndentRule
 import org.gjt.sp.jedit.buffer.JEditBuffer
 
 
-object Token_Markup
-{
+object Token_Markup {
   /* line context */
 
   def mode_rule_set(mode: String): ParserRuleSet =
     new ParserRuleSet(mode, "MAIN")
 
-  object Line_Context
-  {
+  object Line_Context {
     def init(mode: String): Line_Context =
       new Line_Context(mode, Some(Scan.Finished), Line_Structure.init)
 
     def refresh(buffer: JEditBuffer, line: Int): Unit =
       buffer.markTokens(line, DummyTokenHandler.INSTANCE)
 
     def before(buffer: JEditBuffer, line: Int): Line_Context =
       if (line == 0) init(JEdit_Lib.buffer_mode(buffer))
       else after(buffer, line - 1)
 
-    def after(buffer: JEditBuffer, line: Int): Line_Context =
-    {
+    def after(buffer: JEditBuffer, line: Int): Line_Context = {
       val line_mgr = JEdit_Lib.buffer_line_manager(buffer)
       def context =
         line_mgr.getLineContext(line) match {
           case c: Line_Context => Some(c)
           case _ => None

       }
     }
   }
 
   class Line_Context(
-      val mode: String,
-      val context: Option[Scan.Line_Context],
-      val structure: Line_Structure)
-    extends TokenMarker.LineContext(mode_rule_set(mode), null)
-  {
+    val mode: String,
+    val context: Option[Scan.Line_Context],
+    val structure: Line_Structure)
+  extends TokenMarker.LineContext(mode_rule_set(mode), null) {
     def get_context: Scan.Line_Context = context.getOrElse(Scan.Finished)
 
     override def hashCode: Int = (mode, context, structure).hashCode
     override def equals(that: Any): Boolean =
       that match {

   }
 
 
   /* tokens from line (inclusive) */
 
-  private def try_line_tokens(syntax: Outer_Syntax, buffer: JEditBuffer, line: Int)
-    : Option[List[Token]] =
-  {
+  private def try_line_tokens(
+    syntax: Outer_Syntax,
+    buffer: JEditBuffer,
+    line: Int
+  ): Option[List[Token]] = {
     val line_context = Line_Context.before(buffer, line)
     for {
       ctxt <- line_context.context
       text <- JEdit_Lib.get_text(buffer, JEdit_Lib.line_range(buffer, line))
     } yield Token.explode_line(syntax.keywords, text, ctxt)._1

     else Iterator.empty
 
 
   /* command spans */
 
-  def command_span(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset)
-    : Option[Text.Info[Command_Span.Span]] =
-  {
+  def command_span(
+    syntax: Outer_Syntax,
+    buffer: JEditBuffer,
+    offset: Text.Offset
+  ): Option[Text.Info[Command_Span.Span]] = {
     val keywords = syntax.keywords
 
     def maybe_command_start(i: Text.Offset): Option[Text.Info[Token]] =
       token_reverse_iterator(syntax, buffer, i).
         find(info => keywords.is_before_command(info.info) || info.info.is_command)

     def maybe_command_stop(i: Text.Offset): Option[Text.Info[Token]] =
       token_iterator(syntax, buffer, i).
         find(info => keywords.is_before_command(info.info) || info.info.is_command)
 
     if (JEdit_Lib.buffer_range(buffer).contains(offset)) {
-      val start_info =
-      {
+      val start_info = {
         val info1 = maybe_command_start(offset)
         info1 match {
           case Some(Text.Info(range1, tok1)) if tok1.is_command =>
             val info2 = maybe_command_start(range1.start - 1)
             info2 match {

           case Some(Text.Info(range, tok)) =>
             (keywords.is_before_command(tok), range.start, range.stop)
           case None => (false, 0, 0)
         }
 
-      val stop_info =
-      {
+      val stop_info = {
         val info1 = maybe_command_stop(start_next)
         info1 match {
           case Some(Text.Info(range1, tok1)) if tok1.is_command && start_before_command =>
             maybe_command_stop(range1.stop)
           case _ => info1

     }
     else None
   }
 
   private def _command_span_iterator(
-      syntax: Outer_Syntax,
-      buffer: JEditBuffer,
-      offset: Text.Offset,
-      next_offset: Text.Range => Text.Offset): Iterator[Text.Info[Command_Span.Span]] =
-    new Iterator[Text.Info[Command_Span.Span]]
-    {
+    syntax: Outer_Syntax,
+    buffer: JEditBuffer,
+    offset: Text.Offset,
+    next_offset: Text.Range => Text.Offset
+  ): Iterator[Text.Info[Command_Span.Span]] = {
+    new Iterator[Text.Info[Command_Span.Span]] {
       private var next_span = command_span(syntax, buffer, offset)
       def hasNext: Boolean = next_span.isDefined
-      def next(): Text.Info[Command_Span.Span] =
-      {
+      def next(): Text.Info[Command_Span.Span] = {
         val span = next_span.getOrElse(Iterator.empty.next())
         next_span = command_span(syntax, buffer, next_offset(span.range))
         span
       }
     }
+  }
 
   def command_span_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset)
       : Iterator[Text.Info[Command_Span.Span]] =
     _command_span_iterator(syntax, buffer, offset max 0, range => range.stop)
 

 
   /* token marker */
 
   class Marker(
     protected val mode: String,
-    protected val opt_buffer: Option[Buffer]) extends TokenMarker
-  {
+    protected val opt_buffer: Option[Buffer]
+  ) extends TokenMarker {
     addRuleSet(mode_rule_set(mode))
 
     override def hashCode: Int = (mode, opt_buffer).hashCode
     override def equals(that: Any): Boolean =
       that match {

       opt_buffer match {
         case None => "Marker(" + mode + ")"
         case Some(buffer) => "Marker(" + mode + "," + JEdit_Lib.buffer_name(buffer) + ")"
       }
 
-    override def markTokens(context: TokenMarker.LineContext,
-        handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
-    {
+    override def markTokens(
+      context: TokenMarker.LineContext,
+      handler: TokenHandler,
+      raw_line: Segment
+    ): TokenMarker.LineContext = {
       val line = if (raw_line == null) new Segment else raw_line
       val line_context =
         context match { case c: Line_Context => c case _ => Line_Context.init(mode) }
       val structure = line_context.structure
 
-      val context1 =
-      {
+      val context1 = {
         val opt_syntax =
           opt_buffer match {
             case Some(buffer) => Isabelle.buffer_syntax(buffer)
             case None => Isabelle.mode_syntax(mode)
           }

   }
 
 
   /* mode provider */
 
-  class Mode_Provider(orig_provider: ModeProvider) extends ModeProvider
-  {
+  class Mode_Provider(orig_provider: ModeProvider) extends ModeProvider {
     for (mode <- orig_provider.getModes) addMode(mode)
 
-    override def loadMode(mode: Mode, xmh: XModeHandler): Unit =
-    {
+    override def loadMode(mode: Mode, xmh: XModeHandler): Unit = {
       super.loadMode(mode, xmh)
       Isabelle.mode_token_marker(mode.getName).foreach(mode.setTokenMarker)
       Isabelle.indent_rule(mode.getName).foreach(indent_rule =>
         Untyped.set[JList[IndentRule]](mode, "indentRules", JList.of(indent_rule)))
     }