author | wenzelm |
Mon, 26 Dec 2016 13:21:08 +0100 | |
changeset 64671 | 93e375bd3283 |
parent 64667 | cdb0d559a24b |
child 64672 | d8e0619abb60 |
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 = |
|
64671 | 24 |
if (is_theory) |
25 |
session.resources.check_thy_reader( |
|
26 |
"", node_name, new CharSequenceReader(Thy_Header.header_text(doc)), Token.Pos.command) |
|
64605 | 27 |
else Document.Node.no_header |
28 |
||
29 |
||
30 |
/* edits */ |
|
31 |
||
32 |
def text_edits: List[Text.Edit] = |
|
33 |
if (changed) List(Text.Edit.insert(0, doc.text)) else Nil |
|
34 |
||
35 |
def node_edits: List[Document.Edit_Text] = |
|
36 |
if (changed) { |
|
37 |
List(session.header_edit(node_name, node_header), |
|
38 |
node_name -> Document.Node.Clear(), |
|
39 |
node_name -> Document.Node.Edits(text_edits), |
|
40 |
node_name -> |
|
41 |
Document.Node.Perspective(true, Text.Perspective.full, Document.Node.Overlays.empty)) |
|
42 |
} |
|
43 |
else Nil |
|
44 |
||
45 |
def unchanged: Document_Model = if (changed) copy(changed = false) else this |
|
46 |
||
47 |
||
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
64605
diff
changeset
|
48 |
/* snapshot and rendering */ |
64605 | 49 |
|
50 |
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
|
51 |
|
64667 | 52 |
def rendering(options: Options, text_length: Length): VSCode_Rendering = |
53 |
new VSCode_Rendering(this, snapshot(), options, text_length, session.resources) |
|
64605 | 54 |
} |