src/Tools/VSCode/src/vscode_resources.scala
author wenzelm
Wed Apr 12 22:32:55 2017 +0200 (2017-04-12 ago)
changeset 65471 05e5bffcf1d8
parent 65452 9e9750a7932c
child 65472 f83081bcdd0e
permissions -rw-r--r--
clarified loaded_theories: map to qualified theory name;
proper theory_name for PIDE editors;
     1 /*  Title:      Tools/VSCode/src/vscode_resources.scala
     2     Author:     Makarius
     3 
     4 Resources for VSCode Language Server: file-system access and global state.
     5 */
     6 
     7 package isabelle.vscode
     8 
     9 
    10 import isabelle._
    11 
    12 import java.io.{File => JFile}
    13 
    14 import scala.util.parsing.input.Reader
    15 
    16 
    17 object VSCode_Resources
    18 {
    19   /* internal state */
    20 
    21   sealed case class State(
    22     models: Map[JFile, Document_Model] = Map.empty,
    23     pending_input: Set[JFile] = Set.empty,
    24     pending_output: Set[JFile] = Set.empty,
    25     caret: Option[(JFile, Line.Position)] = None)
    26   {
    27     def update_models(changed: Traversable[(JFile, Document_Model)]): State =
    28       copy(
    29         models = models ++ changed,
    30         pending_input = (pending_input /: changed) { case (set, (file, _)) => set + file },
    31         pending_output = (pending_output /: changed) { case (set, (file, _)) => set + file })
    32 
    33     lazy val document_blobs: Document.Blobs =
    34       Document.Blobs(
    35         (for {
    36           (_, model) <- models.iterator
    37           blob <- model.get_blob
    38         } yield (model.node_name -> blob)).toMap)
    39   }
    40 }
    41 
    42 class VSCode_Resources(
    43     val options: Options,
    44     session_base: Sessions.Base,
    45     log: Logger = No_Logger)
    46   extends Resources(session_base, log = log)
    47 {
    48   private val state = Synchronized(VSCode_Resources.State())
    49 
    50 
    51   /* options */
    52 
    53   def pide_extensions: Boolean = options.bool("vscode_pide_extensions")
    54   def unicode_symbols: Boolean = options.bool("vscode_unicode_symbols")
    55   def tooltip_margin: Int = options.int("vscode_tooltip_margin")
    56   def message_margin: Int = options.int("vscode_message_margin")
    57 
    58 
    59   /* document node name */
    60 
    61   def node_file(name: Document.Node.Name): JFile = new JFile(name.node)
    62 
    63   def node_name(file: JFile): Document.Node.Name =
    64   {
    65     val node = file.getPath
    66     val (loaded, theory) = theory_name(default_qualifier, Thy_Header.theory_name(node))
    67     if (loaded) Document.Node.Name.loaded_theory(theory)
    68     else Document.Node.Name(node, if (theory == "") "" else file.getParent, theory)
    69   }
    70 
    71   override def append(dir: String, source_path: Path): String =
    72   {
    73     val path = source_path.expand
    74     if (dir == "" || path.is_absolute) File.platform_path(path)
    75     else if (path.is_current) dir
    76     else if (path.is_basic && !dir.endsWith("/") && !dir.endsWith(JFile.separator))
    77       dir + JFile.separator + File.platform_path(path)
    78     else if (path.is_basic) dir + File.platform_path(path)
    79     else new JFile(dir + JFile.separator + File.platform_path(path)).getCanonicalPath
    80   }
    81 
    82   def get_model(file: JFile): Option[Document_Model] = state.value.models.get(file)
    83   def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name))
    84 
    85 
    86   /* file content */
    87 
    88   def read_file_content(file: JFile): Option[String] =
    89     try { Some(Line.normalize(File.read(file))) }
    90     catch { case ERROR(_) => None }
    91 
    92   def get_file_content(file: JFile): Option[String] =
    93     get_model(file) match {
    94       case Some(model) => Some(model.content.text)
    95       case None => read_file_content(file)
    96     }
    97 
    98   def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
    99     for {
   100       (_, model) <- state.value.models.iterator
   101       info <- model.content.bibtex_entries.iterator
   102     } yield info.map((_, model))
   103 
   104   override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
   105   {
   106     val file = node_file(name)
   107     get_model(file) match {
   108       case Some(model) => f(Scan.char_reader(model.content.text))
   109       case None if file.isFile =>
   110         val reader = Scan.byte_reader(file)
   111         try { f(reader) } finally { reader.close }
   112       case None =>
   113         error("No such file: " + quote(file.toString))
   114     }
   115   }
   116 
   117 
   118   /* document models */
   119 
   120   def visible_node(name: Document.Node.Name): Boolean =
   121     get_model(name) match {
   122       case Some(model) => model.node_visible
   123       case None => false
   124     }
   125 
   126   def change_model(session: Session, file: JFile, text: String, range: Option[Line.Range] = None)
   127   {
   128     state.change(st =>
   129       {
   130         val model = st.models.getOrElse(file, Document_Model.init(session, node_name(file)))
   131         val model1 = (model.change_text(text, range) getOrElse model).external(false)
   132         st.update_models(Some(file -> model1))
   133       })
   134   }
   135 
   136   def close_model(file: JFile): Boolean =
   137     state.change_result(st =>
   138       st.models.get(file) match {
   139         case None => (false, st)
   140         case Some(model) => (true, st.update_models(Some(file -> model.external(true))))
   141       })
   142 
   143   def sync_models(changed_files: Set[JFile]): Unit =
   144     state.change(st =>
   145       {
   146         val changed_models =
   147           (for {
   148             (file, model) <- st.models.iterator
   149             if changed_files(file) && model.external_file
   150             text <- read_file_content(file)
   151             model1 <- model.change_text(text)
   152           } yield (file, model1)).toList
   153         st.update_models(changed_models)
   154       })
   155 
   156 
   157   /* resolve dependencies */
   158 
   159   def resolve_dependencies(session: Session, file_watcher: File_Watcher): (Boolean, Boolean) =
   160   {
   161     state.change_result(st =>
   162       {
   163         /* theory files */
   164 
   165         val thys =
   166           (for ((_, model) <- st.models.iterator if model.is_theory)
   167            yield (model.node_name, Position.none)).toList
   168 
   169         val thy_files = thy_info.dependencies(thys).deps.map(_.name)
   170 
   171 
   172         /* auxiliary files */
   173 
   174         val stable_tip_version =
   175           if (st.models.forall(entry => entry._2.is_stable))
   176             session.current_state().stable_tip_version
   177           else None
   178 
   179         val aux_files =
   180           stable_tip_version match {
   181             case Some(version) => undefined_blobs(version.nodes)
   182             case None => Nil
   183           }
   184 
   185 
   186         /* loaded models */
   187 
   188         val loaded_models =
   189           (for {
   190             node_name <- thy_files.iterator ++ aux_files.iterator
   191             file = node_file(node_name)
   192             if !st.models.isDefinedAt(file)
   193             text <- { file_watcher.register_parent(file); read_file_content(file) }
   194           }
   195           yield {
   196             val model = Document_Model.init(session, node_name)
   197             val model1 = (model.change_text(text) getOrElse model).external(true)
   198             (file, model1)
   199           }).toList
   200 
   201         val invoke_input = loaded_models.nonEmpty
   202         val invoke_load = stable_tip_version.isEmpty
   203 
   204         ((invoke_input, invoke_load), st.update_models(loaded_models))
   205       })
   206   }
   207 
   208 
   209   /* pending input */
   210 
   211   def flush_input(session: Session)
   212   {
   213     state.change(st =>
   214       {
   215         val changed_models =
   216           (for {
   217             file <- st.pending_input.iterator
   218             model <- st.models.get(file)
   219             (edits, model1) <- model.flush_edits(st.document_blobs)
   220           } yield (edits, (file, model1))).toList
   221 
   222         session.update(st.document_blobs, changed_models.flatMap(_._1))
   223         st.copy(
   224           models = st.models ++ changed_models.iterator.map(_._2),
   225           pending_input = Set.empty)
   226       })
   227   }
   228 
   229 
   230   /* pending output */
   231 
   232   def update_output(changed_nodes: Traversable[JFile]): Unit =
   233     state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes))
   234 
   235   def flush_output(channel: Channel): Boolean =
   236   {
   237     state.change_result(st =>
   238       {
   239         val (postponed, flushed) =
   240           (for {
   241             file <- st.pending_output.iterator
   242             model <- st.models.get(file)
   243           } yield (file, model, model.rendering())).toList.partition(_._3.snapshot.is_outdated)
   244 
   245         val changed_iterator =
   246           for {
   247             (file, model, rendering) <- flushed.iterator
   248             (changed_diags, changed_decos, model1) = model.publish(rendering)
   249             if changed_diags.isDefined || changed_decos.isDefined
   250           }
   251           yield {
   252             for (diags <- changed_diags)
   253               channel.write(Protocol.PublishDiagnostics(file, rendering.diagnostics_output(diags)))
   254             if (pide_extensions) {
   255               for (decos <- changed_decos; deco <- decos)
   256                 channel.write(rendering.decoration_output(deco).json(file))
   257             }
   258             (file, model1)
   259           }
   260 
   261         (postponed.nonEmpty,
   262           st.copy(
   263             models = st.models ++ changed_iterator,
   264             pending_output = postponed.map(_._1).toSet))
   265       }
   266     )
   267   }
   268 
   269 
   270   /* output text */
   271 
   272   def output_text(s: String): String =
   273     if (unicode_symbols) Symbol.decode(s) else Symbol.encode(s)
   274 
   275   def output_xml(xml: XML.Tree): String =
   276     output_text(XML.content(xml))
   277 
   278   def output_pretty(body: XML.Body, margin: Int): String =
   279     output_text(Pretty.string_of(body, margin))
   280   def output_pretty_tooltip(body: XML.Body): String = output_pretty(body, tooltip_margin)
   281   def output_pretty_message(body: XML.Body): String = output_pretty(body, message_margin)
   282 
   283 
   284   /* caret handling */
   285 
   286   def update_caret(caret: Option[(JFile, Line.Position)])
   287   { state.change(_.copy(caret = caret)) }
   288 
   289   def caret_offset(): Option[(Document_Model, Text.Offset)] =
   290   {
   291     val st = state.value
   292     for {
   293       (file, pos) <- st.caret
   294       model <- st.models.get(file)
   295       offset <- model.content.doc.offset(pos)
   296     }
   297     yield (model, offset)
   298   }
   299 
   300 
   301   /* spell checker */
   302 
   303   val spell_checker = new Spell_Checker_Variable
   304   spell_checker.update(options)
   305 }