/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/ |
H A D | document_model.scala | 35 (node_name, model) <- models.iterator 37 } yield (node_name, model.asInstanceOf[File_Model]) 42 (node_name, model) <- models.iterator 44 } yield (node_name -> blob)).toMap) 46 def open_buffer(session: Session, node_name: Document.Node.Name, buffer: Buffer) 50 models.get(node_name) match { 55 val buffer_model = Buffer_Model(session, node_name, buffer).init(old_model) 57 copy(models = models + (node_name -> buffer_model), 67 copy(models = models + (file_model.node_name -> file_model), 72 def provide_file(session: Session, node_name [all...] |
H A D | jedit_resources.scala | 42 def node_name(path: String): Document.Node.Name = 54 def node_name(buffer: Buffer): Document.Node.Name = 55 node_name(JEdit_Lib.buffer_name(buffer)) 59 val name = node_name(buffer) 81 def read_file_content(node_name: Document.Node.Name): Option[String] = 83 Bibtex.make_theory_content(node_name.theory) orElse { 84 val name = node_name.node 95 def get_file_content(node_name: Document.Node.Name): Option[String] = 96 Document_Model.get(node_name) match { 99 case None => read_file_content(node_name) [all...] |
H A D | jedit_editor.scala | 53 } yield doc_view.model.node_name).contains(name) 59 GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.node_name) } 82 snapshot.current_command(doc_view.model.node_name, text_area.getCaretPosition) 86 snapshot.version.nodes.commands_loading(model.node_name).headOption 231 catch { case ERROR(_) => Line.Node_Position(file_model.node_name.node) } 236 override def toString: String = "buffer " + quote(model.node_name.node) 248 PIDE.resources.get_file_content(PIDE.resources.node_name(name)) match { 276 case Some((node, command)) if snapshot.version.nodes(command.node_name) eq node =>
|
H A D | pretty_text_area.scala | 38 val node_name = command.node_name 40 List(node_name -> Document.Node.Edits(List(Text.Edit.insert(0, command.source)))) 46 val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command)))
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/ |
H A D | document_model.scala | 35 (node_name, model) <- models.iterator 37 } yield (node_name, model.asInstanceOf[File_Model]) 42 (node_name, model) <- models.iterator 44 } yield (node_name -> blob)).toMap) 46 def open_buffer(session: Session, node_name: Document.Node.Name, buffer: Buffer) 50 models.get(node_name) match { 55 val buffer_model = Buffer_Model(session, node_name, buffer).init(old_model) 57 copy(models = models + (node_name -> buffer_model), 67 copy(models = models + (file_model.node_name -> file_model), 72 def provide_file(session: Session, node_name [all...] |
H A D | jedit_resources.scala | 42 def node_name(path: String): Document.Node.Name = 54 def node_name(buffer: Buffer): Document.Node.Name = 55 node_name(JEdit_Lib.buffer_name(buffer)) 59 val name = node_name(buffer) 81 def read_file_content(node_name: Document.Node.Name): Option[String] = 83 Bibtex.make_theory_content(node_name.theory) orElse { 84 val name = node_name.node 95 def get_file_content(node_name: Document.Node.Name): Option[String] = 96 Document_Model.get(node_name) match { 99 case None => read_file_content(node_name) [all...] |
H A D | jedit_editor.scala | 53 } yield doc_view.model.node_name).contains(name) 59 GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.node_name) } 82 snapshot.current_command(doc_view.model.node_name, text_area.getCaretPosition) 86 snapshot.version.nodes.commands_loading(model.node_name).headOption 231 catch { case ERROR(_) => Line.Node_Position(file_model.node_name.node) } 236 override def toString: String = "buffer " + quote(model.node_name.node) 248 PIDE.resources.get_file_content(PIDE.resources.node_name(name)) match { 276 case Some((node, command)) if snapshot.version.nodes(command.node_name) eq node =>
|
H A D | pretty_text_area.scala | 38 val node_name = command.node_name 40 List(node_name -> Document.Node.Edits(List(Text.Edit.insert(0, command.source)))) 46 val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command)))
|
/seL4-l4v-10.1.1/isabelle/src/Pure/Thy/ |
H A D | thy_resources.scala | 66 def snapshot(node_name: Document.Node.Name): Document.Snapshot = 68 val snapshot = state.snapshot(node_name) 151 yield command.node_name).toSet 232 val node_name: Document.Node.Name, 237 override def toString: String = node_name.toString 243 List(node_name -> Document.Node.Deps(node_header), 244 node_name -> Document.Node.Edits(text_edits), 245 node_name -> node_perspective) 262 else new Theory(node_name, node_header, text, required) 286 for (node_name < [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Thy/ |
H A D | thy_resources.scala | 66 def snapshot(node_name: Document.Node.Name): Document.Snapshot = 68 val snapshot = state.snapshot(node_name) 151 yield command.node_name).toSet 232 val node_name: Document.Node.Name, 237 override def toString: String = node_name.toString 243 List(node_name -> Document.Node.Deps(node_header), 244 node_name -> Document.Node.Edits(text_edits), 245 node_name -> node_perspective) 262 else new Theory(node_name, node_header, text, required) 286 for (node_name < [all...] |
/seL4-l4v-10.1.1/isabelle/src/Tools/VSCode/src/ |
H A D | document_model.scala | 60 def init(session: Session, editor: Server.Editor, node_name: Document.Node.Name): Document_Model = 61 Document_Model(session, editor, node_name, Content.empty, 62 node_required = node_name.is_bibtex_theory) 68 node_name: Document.Node.Name, 98 resources.special_header(node_name) getOrElse 99 resources.check_thy_reader(node_name, Scan.char_reader(content.text)) 134 val overlays = editor.node_overlays(node_name) 234 def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits) 244 if (is_theory) session.recent_syntax(node_name) else Outer_Syntax.empty
|
H A D | vscode_resources.scala | 52 } yield (model.node_name -> blob)).toMap) 68 def node_name: Document.Node.Name = model.node_name 95 def node_name(file: JFile): Document.Node.Name = 170 val model = st.models.getOrElse(file, Document_Model.init(session, editor, node_name(file))) 204 state.change(_.change_overlay(true, node_file(command.node_name), command, fn, args)) 207 state.change(_.change_overlay(false, node_file(command.node_name), command, fn, args)) 223 yield (model.node_name, Position.none)).toList 229 (_, model) <- st.models.iterator if model.node_name.is_bibtex 230 thy_name <- Bibtex.make_theory_name(resources, model.node_name) [all...] |
H A D | dynamic_output.scala | 26 snapshot.current_command(caret.node_name, caret.offset) match {
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/VSCode/src/ |
H A D | document_model.scala | 60 def init(session: Session, editor: Server.Editor, node_name: Document.Node.Name): Document_Model = 61 Document_Model(session, editor, node_name, Content.empty, 62 node_required = node_name.is_bibtex_theory) 68 node_name: Document.Node.Name, 98 resources.special_header(node_name) getOrElse 99 resources.check_thy_reader(node_name, Scan.char_reader(content.text)) 134 val overlays = editor.node_overlays(node_name) 234 def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits) 244 if (is_theory) session.recent_syntax(node_name) else Outer_Syntax.empty
|
H A D | vscode_resources.scala | 52 } yield (model.node_name -> blob)).toMap) 68 def node_name: Document.Node.Name = model.node_name 95 def node_name(file: JFile): Document.Node.Name = 170 val model = st.models.getOrElse(file, Document_Model.init(session, editor, node_name(file))) 204 state.change(_.change_overlay(true, node_file(command.node_name), command, fn, args)) 207 state.change(_.change_overlay(false, node_file(command.node_name), command, fn, args)) 223 yield (model.node_name, Position.none)).toList 229 (_, model) <- st.models.iterator if model.node_name.is_bibtex 230 thy_name <- Bibtex.make_theory_name(resources, model.node_name) [all...] |
/seL4-l4v-10.1.1/isabelle/src/Pure/Isar/ |
H A D | document_structure.scala | 35 node_name: Document.Node.Name, 82 spans.foreach(span => add(Command(Document_ID.none, node_name, Command.no_blobs, span))) 159 node_name: Document.Node.Name, 167 Command(Document_ID.none, node_name, Command.no_blobs, span)))
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Isar/ |
H A D | document_structure.scala | 35 node_name: Document.Node.Name, 82 spans.foreach(span => add(Command(Document_ID.none, node_name, Command.no_blobs, span))) 159 node_name: Document.Node.Name, 167 Command(Document_ID.none, node_name, Command.no_blobs, span)))
|
/seL4-l4v-10.1.1/isabelle/src/Pure/PIDE/ |
H A D | resources.scala | 30 def append(node_name: Document.Node.Name, source_path: Path): String = 31 append(node_name.master_dir, source_path) 100 case Some(node_name) => node_name 151 def check_thy_reader(node_name: Document.Node.Name, reader: Reader[Char], 154 if (node_name.is_theory && reader.source.length > 0) { 158 val base_name = node_name.theory_base_name 167 val name = import_name(node_name, s) 205 (node_name, node) <- nodes.iterator 206 if !session_base.loaded_theory(node_name) [all...] |
H A D | document.scala | 37 update(command.node_name, _.insert(command, fn, args)) 40 update(command.node_name, _.remove(command, fn, args)) 135 JSON.Object("node_name" -> node, "theory_name" -> theory) 532 def node_name: Node.Name 579 def node_name: Node.Name 580 def is_theory: Boolean = node_name.is_theory 581 override def toString: String = node_name.toString 587 def is_bibtex: Boolean = node_name.is_bibtex 588 def is_bibtex_theory: Boolean = node_name.is_bibtex_theory 601 if (session.resources.session_base.loaded_theory(node_name)) { [all...] |
H A D | command.scala | 238 (command.id, (command.node_name.node, ((blobs_names, blobs_index), (command.span, 242 def decode(node_name: String => Document.Node.Name): XML.Decode.T[State] = (body: XML.Body) => 250 (blobs_names.map(name => Exn.Res((node_name(name), None)): Blob), blobs_index) 251 val command = Command(id, node_name(node), blobs_info, span) 297 if (command.node_name.theory == entry._2.theory_name) Some(copy(exports = exports + entry)) 399 node_name: Document.Node.Name, 404 new Command(id, node_name, blobs_info, span1, source, Results.empty, Markup_Tree.empty) 492 node_name: Document.Node.Name, 499 val imports = resources.check_thy_reader(node_name, reader).imports 513 val qualifier = resources.session_base.theory_qualifier(node_name) [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/PIDE/ |
H A D | resources.scala | 30 def append(node_name: Document.Node.Name, source_path: Path): String = 31 append(node_name.master_dir, source_path) 100 case Some(node_name) => node_name 151 def check_thy_reader(node_name: Document.Node.Name, reader: Reader[Char], 154 if (node_name.is_theory && reader.source.length > 0) { 158 val base_name = node_name.theory_base_name 167 val name = import_name(node_name, s) 205 (node_name, node) <- nodes.iterator 206 if !session_base.loaded_theory(node_name) [all...] |
H A D | document.scala | 37 update(command.node_name, _.insert(command, fn, args)) 40 update(command.node_name, _.remove(command, fn, args)) 135 JSON.Object("node_name" -> node, "theory_name" -> theory) 532 def node_name: Node.Name 579 def node_name: Node.Name 580 def is_theory: Boolean = node_name.is_theory 581 override def toString: String = node_name.toString 587 def is_bibtex: Boolean = node_name.is_bibtex 588 def is_bibtex_theory: Boolean = node_name.is_bibtex_theory 601 if (session.resources.session_base.loaded_theory(node_name)) { [all...] |
H A D | command.scala | 238 (command.id, (command.node_name.node, ((blobs_names, blobs_index), (command.span, 242 def decode(node_name: String => Document.Node.Name): XML.Decode.T[State] = (body: XML.Body) => 250 (blobs_names.map(name => Exn.Res((node_name(name), None)): Blob), blobs_index) 251 val command = Command(id, node_name(node), blobs_info, span) 297 if (command.node_name.theory == entry._2.theory_name) Some(copy(exports = exports + entry)) 399 node_name: Document.Node.Name, 404 new Command(id, node_name, blobs_info, span1, source, Results.empty, Markup_Tree.empty) 492 node_name: Document.Node.Name, 499 val imports = resources.check_thy_reader(node_name, reader).imports 513 val qualifier = resources.session_base.theory_qualifier(node_name) [all...] |
/seL4-l4v-10.1.1/isabelle/src/Pure/Tools/ |
H A D | dump.scala | 19 node_name: Document.Node.Name, 25 val path = output_dir + Path.basic(node_name.theory) + file_name 128 for ((node_name, node_status) <- theories_result.nodes) { 129 val snapshot = theories_result.snapshot(node_name) 131 Aspect_Args(dump_options, progress, deps, output_dir, node_name, node_status, snapshot)
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Tools/ |
H A D | dump.scala | 19 node_name: Document.Node.Name, 25 val path = output_dir + Path.basic(node_name.theory) + file_name 128 for ((node_name, node_status) <- theories_result.nodes) { 129 val snapshot = theories_result.snapshot(node_name) 131 Aspect_Args(dump_options, progress, deps, output_dir, node_name, node_status, snapshot)
|