object Fold_Handling { /* input: dynamic line context */
class Fold_Handler extends FoldHandler("isabelle") { overridedef equals(other: Any): Boolean =
other match { case that: Fold_Handler => true case _ => false
}
overridedef getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int =
Token_Markup.Line_Context.after(buffer, line).structure.depth max 0
overridedef getPrecedingFoldLevels(
buffer: JEditBuffer,
line: Int,
seg: Segment, level: Int
): JList[Integer] = { val structure = Token_Markup.Line_Context.after(buffer, line).structure val result = if (line > 0 && structure.command)
Range.inclusive(line - 1, 0, -1).iterator.
map(i => Token_Markup.Line_Context.after(buffer, i).structure).
takeWhile(_.improper).map(_ => structure.depth max 0).toList else Nil
if (result.isEmpty) nullelse result.map(Integer.valueOf).asJava
}
}
/* output: static document rendering */
class Document_Fold_Handler(privateval rendering: JEdit_Rendering) extends FoldHandler("isabelle-document") { overridedef equals(other: Any): Boolean =
other match { case that: Document_Fold_Handler => this.rendering == that.rendering case _ => false
}
overridedef getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int = { def depth(i: Text.Offset): Int = if (i < 0) 0 else {
rendering.fold_depth(Text.Range(i, i + 1)) match { case Text.Info(_, d) :: _ => d case _ => 0
}
}
if (line <= 0) 0 else { val range = JEdit_Lib.line_range(buffer, line - 1)
buffer.getFoldLevel(line - 1) - depth(range.start - 1) + depth(range.stop - 1)
}
}
}
}
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
