author | wenzelm |
Wed, 21 Dec 2016 22:27:38 +0100 | |
changeset 64649 | d67c3094a0c2 |
parent 64622 | 529bbb8977c7 |
child 64667 | cdb0d559a24b |
permissions | -rw-r--r-- |
64605 | 1 |
/* Title: Tools/VSCode/src/document_model.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Document model for line-oriented text. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle.vscode |
|
8 |
||
9 |
||
10 |
import isabelle._ |
|
11 |
||
12 |
import scala.util.parsing.input.CharSequenceReader |
|
13 |
||
14 |
||
15 |
case class Document_Model( |
|
16 |
session: Session, doc: Line.Document, node_name: Document.Node.Name, |
|
17 |
changed: Boolean = true) |
|
18 |
{ |
|
19 |
/* header */ |
|
20 |
||
21 |
def is_theory: Boolean = node_name.is_theory |
|
22 |
||
23 |
lazy val node_header: Document.Node.Header = |
|
24 |
if (is_theory) { |
|
25 |
val toks = Token.explode(Thy_Header.bootstrap_syntax.keywords, doc.text) |
|
26 |
val toks1 = toks.dropWhile(tok => !tok.is_command(Thy_Header.THEORY)) |
|
27 |
toks1.iterator.zipWithIndex.collectFirst({ case (tok, i) if tok.is_begin => i }) match { |
|
28 |
case Some(i) => |
|
29 |
session.resources.check_thy_reader("", node_name, |
|
30 |
new CharSequenceReader(toks1.take(i + 1).map(_.source).mkString), Token.Pos.command) |
|
31 |
case None => Document.Node.no_header |
|
32 |
} |
|
33 |
} |
|
34 |
else Document.Node.no_header |
|
35 |
||
36 |
||
37 |
/* edits */ |
|
38 |
||
39 |
def text_edits: List[Text.Edit] = |
|
40 |
if (changed) List(Text.Edit.insert(0, doc.text)) else Nil |
|
41 |
||
42 |
def node_edits: List[Document.Edit_Text] = |
|
43 |
if (changed) { |
|
44 |
List(session.header_edit(node_name, node_header), |
|
45 |
node_name -> Document.Node.Clear(), |
|
46 |
node_name -> Document.Node.Edits(text_edits), |
|
47 |
node_name -> |
|
48 |
Document.Node.Perspective(true, Text.Perspective.full, Document.Node.Overlays.empty)) |
|
49 |
} |
|
50 |
else Nil |
|
51 |
||
52 |
def unchanged: Document_Model = if (changed) copy(changed = false) else this |
|
53 |
||
54 |
||
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
64605
diff
changeset
|
55 |
/* snapshot and rendering */ |
64605 | 56 |
|
57 |
def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits) |
|
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
64605
diff
changeset
|
58 |
|
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
64605
diff
changeset
|
59 |
def rendering(options: Options): VSCode_Rendering = |
64649 | 60 |
new VSCode_Rendering(this, snapshot(), options, session.resources) |
64605 | 61 |
} |