# HG changeset patch # User wenzelm # Date 1468251951 -7200 # Node ID 8191c3e9f2d32ede939e77df94d41ecd4e342851 # Parent c037248d54e89efa08edaa8643c2fcff1ad1837b support more modes; diff -r c037248d54e8 -r 8191c3e9f2d3 src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Mon Jul 11 17:08:04 2016 +0200 +++ b/src/Tools/jEdit/src/isabelle.scala Mon Jul 11 17:45:51 2016 +0200 @@ -87,7 +87,11 @@ /* text structure */ def indent_rule(mode: String): Option[IndentRule] = - if (mode == "isabelle") Some(Text_Structure.Indent_Rule) else None + mode match { + case "isabelle" | "isabelle-options" | "isabelle-root" => + Some(Text_Structure.Indent_Rule) + case _ => None + } def structure_matchers(mode: String): List[StructureMatcher] = if (mode == "isabelle") List(Text_Structure.Matcher) else Nil diff -r c037248d54e8 -r 8191c3e9f2d3 src/Tools/jEdit/src/token_markup.scala --- a/src/Tools/jEdit/src/token_markup.scala Mon Jul 11 17:08:04 2016 +0200 +++ b/src/Tools/jEdit/src/token_markup.scala Mon Jul 11 17:45:51 2016 +0200 @@ -175,22 +175,23 @@ /* line context */ - private val context_rules = new ParserRuleSet("isabelle", "MAIN") - object Line_Context { - val init = new Line_Context(Some(Scan.Finished), Outer_Syntax.Line_Structure.init) + def init(mode: String): Line_Context = + new Line_Context(mode, Some(Scan.Finished), Outer_Syntax.Line_Structure.init) } class Line_Context( + val mode: String, val context: Option[Scan.Line_Context], val structure: Outer_Syntax.Line_Structure) - extends TokenMarker.LineContext(context_rules, null) + extends TokenMarker.LineContext(new ParserRuleSet(mode, "MAIN"), null) { - override def hashCode: Int = (context, structure).hashCode + override def hashCode: Int = (mode, context, structure).hashCode override def equals(that: Any): Boolean = that match { - case other: Line_Context => context == other.context && structure == other.structure + case other: Line_Context => + mode == other.mode && context == other.context && structure == other.structure case _ => false } } @@ -205,7 +206,7 @@ } context getOrElse { buffer.markTokens(line, DummyTokenHandler.INSTANCE) - context getOrElse Line_Context.init + context getOrElse Line_Context.init(JEdit_Lib.buffer_mode(buffer)) } } @@ -216,7 +217,7 @@ : Option[List[Token]] = { val line_context = - if (line == 0) Line_Context.init + if (line == 0) Line_Context.init(JEdit_Lib.buffer_mode(buffer)) else buffer_line_context(buffer, line - 1) for { ctxt <- line_context.context @@ -381,7 +382,8 @@ 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 } + val line_context = + context match { case c: Line_Context => c case _ => Line_Context.init(mode) } val structure = line_context.structure val context1 = @@ -396,18 +398,18 @@ case (Some(ctxt), _) if mode == "isabelle-ml" || mode == "sml" => val (tokens, ctxt1) = ML_Lex.tokenize_line(mode == "sml", line, ctxt) val styled_tokens = tokens.map(tok => (Rendering.ml_token_markup(tok), tok.source)) - (styled_tokens, new Line_Context(Some(ctxt1), structure)) + (styled_tokens, new Line_Context(line_context.mode, Some(ctxt1), structure)) case (Some(ctxt), Some(syntax)) if syntax.has_tokens => val (tokens, ctxt1) = Token.explode_line(syntax.keywords, line, ctxt) val structure1 = syntax.line_structure(tokens, structure) val styled_tokens = tokens.map(tok => (Rendering.token_markup(syntax, tok), tok.source)) - (styled_tokens, new Line_Context(Some(ctxt1), structure1)) + (styled_tokens, new Line_Context(line_context.mode, Some(ctxt1), structure1)) case _ => val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString) - (List(styled_token), new Line_Context(None, structure)) + (List(styled_token), new Line_Context(line_context.mode, None, structure)) } val extended = extended_styles(line)