10 import isabelle._ |
10 import isabelle._ |
11 |
11 |
12 import org.gjt.sp.jedit.indent.{IndentRule, IndentAction} |
12 import org.gjt.sp.jedit.indent.{IndentRule, IndentAction} |
13 import org.gjt.sp.jedit.textarea.{TextArea, StructureMatcher, Selection} |
13 import org.gjt.sp.jedit.textarea.{TextArea, StructureMatcher, Selection} |
14 import org.gjt.sp.jedit.buffer.JEditBuffer |
14 import org.gjt.sp.jedit.buffer.JEditBuffer |
|
15 import org.gjt.sp.jedit.Buffer |
15 |
16 |
16 |
17 |
17 object Text_Structure |
18 object Text_Structure |
18 { |
19 { |
19 /* indentation */ |
20 /* indentation */ |
20 |
21 |
21 object Indent_Rule extends IndentRule |
22 object Indent_Rule extends IndentRule |
22 { |
23 { |
23 def apply(buffer: JEditBuffer, this_line: Int, prev_line: Int, prev_prev_line: Int, |
24 def apply(buffer0: JEditBuffer, line: Int, prev_line: Int, prev_prev_line: Int, |
24 actions: java.util.List[IndentAction]) |
25 actions: java.util.List[IndentAction]) |
25 { |
26 { |
26 val indent = 0 // FIXME |
27 buffer0 match { |
|
28 case buffer: Buffer => |
|
29 Isabelle.buffer_syntax(buffer) match { |
|
30 case Some(syntax) => |
|
31 val limit = PIDE.options.value.int("jedit_structure_limit") max 0 |
27 |
32 |
28 actions.clear() |
33 val indent = 0 // FIXME |
29 actions.add(new IndentAction.AlignOffset(indent)) |
34 |
|
35 actions.clear() |
|
36 actions.add(new IndentAction.AlignOffset(indent)) |
|
37 case _ => |
|
38 } |
|
39 case _ => |
|
40 } |
30 } |
41 } |
31 } |
42 } |
32 |
43 |
33 |
44 |
34 /* structure matching */ |
45 /* structure matching */ |