equal
deleted
inserted
replaced
85 |
85 |
86 |
86 |
87 /* text structure */ |
87 /* text structure */ |
88 |
88 |
89 def indent_rule(mode: String): Option[IndentRule] = |
89 def indent_rule(mode: String): Option[IndentRule] = |
90 if (mode == "isabelle") Some(Text_Structure.Indent_Rule) else None |
90 mode match { |
|
91 case "isabelle" | "isabelle-options" | "isabelle-root" => |
|
92 Some(Text_Structure.Indent_Rule) |
|
93 case _ => None |
|
94 } |
91 |
95 |
92 def structure_matchers(mode: String): List[StructureMatcher] = |
96 def structure_matchers(mode: String): List[StructureMatcher] = |
93 if (mode == "isabelle") List(Text_Structure.Matcher) else Nil |
97 if (mode == "isabelle") List(Text_Structure.Matcher) else Nil |
94 |
98 |
95 |
99 |