58 |
58 |
59 class Document_Model(val session: Session, val buffer: Buffer, val node_name: Document.Node.Name) |
59 class Document_Model(val session: Session, val buffer: Buffer, val node_name: Document.Node.Name) |
60 { |
60 { |
61 /* header */ |
61 /* header */ |
62 |
62 |
|
63 def is_theory: Boolean = node_name.is_theory |
|
64 |
63 def node_header(): Document.Node.Header = |
65 def node_header(): Document.Node.Header = |
64 { |
66 { |
65 Swing_Thread.require() |
67 Swing_Thread.require() |
66 JEdit_Lib.buffer_lock(buffer) { |
68 |
67 Exn.capture { |
69 if (is_theory) { |
68 PIDE.thy_load.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength)) |
70 JEdit_Lib.buffer_lock(buffer) { |
69 } match { |
71 Exn.capture { |
70 case Exn.Res(header) => header |
72 PIDE.thy_load.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength)) |
71 case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn)) |
73 } match { |
|
74 case Exn.Res(header) => header |
|
75 case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn)) |
|
76 } |
72 } |
77 } |
73 } |
78 } |
|
79 else Document.Node.no_header |
74 } |
80 } |
75 |
81 |
76 |
82 |
77 /* perspective */ |
83 /* perspective */ |
78 |
84 |
94 |
100 |
95 def node_perspective(): Document.Node.Perspective_Text = |
101 def node_perspective(): Document.Node.Perspective_Text = |
96 { |
102 { |
97 Swing_Thread.require() |
103 Swing_Thread.require() |
98 |
104 |
99 if (Isabelle.continuous_checking) { |
105 if (Isabelle.continuous_checking && is_theory) { |
100 val snapshot = this.snapshot() |
106 val snapshot = this.snapshot() |
101 Document.Node.Perspective(node_required, Text.Perspective( |
107 Document.Node.Perspective(node_required, Text.Perspective( |
102 for { |
108 for { |
103 doc_view <- PIDE.document_views(buffer) |
109 doc_view <- PIDE.document_views(buffer) |
104 range <- doc_view.perspective(snapshot).ranges |
110 range <- doc_view.perspective(snapshot).ranges |
106 } |
112 } |
107 else empty_perspective |
113 else empty_perspective |
108 } |
114 } |
109 |
115 |
110 |
116 |
|
117 /* blob */ |
|
118 |
|
119 // FIXME caching |
|
120 // FIXME precise file content (encoding) |
|
121 def blob(): Bytes = |
|
122 Swing_Thread.require { Bytes(buffer.getText(0, buffer.getLength)) } |
|
123 |
|
124 |
111 /* edits */ |
125 /* edits */ |
112 |
126 |
113 def init_edits(): List[Document.Edit_Text] = |
127 def init_edits(): List[Document.Edit_Text] = |
114 { |
128 { |
115 Swing_Thread.require() |
129 Swing_Thread.require() |
116 |
130 |
117 val header = node_header() |
131 val header = node_header() |
118 val text = JEdit_Lib.buffer_text(buffer) |
132 val text = JEdit_Lib.buffer_text(buffer) |
119 val perspective = node_perspective() |
133 val perspective = node_perspective() |
120 |
134 |
121 List(session.header_edit(node_name, header), |
135 if (is_theory) |
122 node_name -> Document.Node.Clear(), |
136 List(session.header_edit(node_name, header), |
123 node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))), |
137 node_name -> Document.Node.Clear(), |
124 node_name -> perspective) |
138 node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))), |
|
139 node_name -> perspective) |
|
140 else |
|
141 List(node_name -> Document.Node.Blob(blob())) |
125 } |
142 } |
126 |
143 |
127 def node_edits( |
144 def node_edits( |
128 clear: Boolean, |
145 clear: Boolean, |
129 text_edits: List[Text.Edit], |
146 text_edits: List[Text.Edit], |
130 perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] = |
147 perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] = |
131 { |
148 { |
132 Swing_Thread.require() |
149 Swing_Thread.require() |
133 |
150 |
134 val header_edit = session.header_edit(node_name, node_header()) |
151 if (is_theory) { |
135 if (clear) |
152 val header_edit = session.header_edit(node_name, node_header()) |
136 List(header_edit, |
153 if (clear) |
137 node_name -> Document.Node.Clear(), |
154 List(header_edit, |
138 node_name -> Document.Node.Edits(text_edits), |
155 node_name -> Document.Node.Clear(), |
139 node_name -> perspective) |
156 node_name -> Document.Node.Edits(text_edits), |
|
157 node_name -> perspective) |
|
158 else |
|
159 List(header_edit, |
|
160 node_name -> Document.Node.Edits(text_edits), |
|
161 node_name -> perspective) |
|
162 } |
140 else |
163 else |
141 List(header_edit, |
164 List(node_name -> Document.Node.Blob(blob())) |
142 node_name -> Document.Node.Edits(text_edits), |
|
143 node_name -> perspective) |
|
144 } |
165 } |
145 |
166 |
146 |
167 |
147 /* pending edits */ |
168 /* pending edits */ |
148 |
169 |