src/Tools/VSCode/src/vscode_resources.scala
author wenzelm
Fri Apr 21 14:09:03 2017 +0200 (2017-04-21 ago)
changeset 65532 febfd9f78bd4
parent 65524 0910f1733909
child 65926 0f7821a07aa9
permissions -rw-r--r--
eliminated default_qualifier: just a constant;
     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     session_base.known.get_file(file) getOrElse {
    65       val node = file.getPath
    66       theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) match {
    67         case (true, theory) => Document.Node.Name.loaded_theory(theory)
    68         case (false, theory) =>
    69           val master_dir = if (theory == "") "" else file.getParent
    70           Document.Node.Name(node, master_dir, theory)
    71       }
    72     }
    73 
    74   override def append(dir: String, source_path: Path): String =
    75   {
    76     val path = source_path.expand
    77     if (dir == "" || path.is_absolute) File.platform_path(path)
    78     else if (path.is_current) dir
    79     else if (path.is_basic && !dir.endsWith("/") && !dir.endsWith(JFile.separator))
    80       dir + JFile.separator + File.platform_path(path)
    81     else if (path.is_basic) dir + File.platform_path(path)
    82     else new JFile(dir + JFile.separator + File.platform_path(path)).getCanonicalPath
    83   }
    84 
    85   def get_model(file: JFile): Option[Document_Model] = state.value.models.get(file)
    86   def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name))
    87 
    88 
    89   /* file content */
    90 
    91   def read_file_content(file: JFile): Option[String] =
    92     try { Some(Line.normalize(File.read(file))) }
    93     catch { case ERROR(_) => None }
    94 
    95   def get_file_content(file: JFile): Option[String] =
    96     get_model(file) match {
    97       case Some(model) => Some(model.content.text)
    98       case None => read_file_content(file)
    99     }
   100 
   101   def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
   102     for {
   103       (_, model) <- state.value.models.iterator
   104       info <- model.content.bibtex_entries.iterator
   105     } yield info.map((_, model))
   106 
   107   override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
   108   {
   109     val file = node_file(name)
   110     get_model(file) match {
   111       case Some(model) => f(Scan.char_reader(model.content.text))
   112       case None if file.isFile =>
   113         val reader = Scan.byte_reader(file)
   114         try { f(reader) } finally { reader.close }
   115       case None =>
   116         error("No such file: " + quote(file.toString))
   117     }
   118   }
   119 
   120 
   121   /* document models */
   122 
   123   def visible_node(name: Document.Node.Name): Boolean =
   124     get_model(name) match {
   125       case Some(model) => model.node_visible
   126       case None => false
   127     }
   128 
   129   def change_model(session: Session, file: JFile, text: String, range: Option[Line.Range] = None)
   130   {
   131     state.change(st =>
   132       {
   133         val model = st.models.getOrElse(file, Document_Model.init(session, node_name(file)))
   134         val model1 = (model.change_text(text, range) getOrElse model).external(false)
   135         st.update_models(Some(file -> model1))
   136       })
   137   }
   138 
   139   def close_model(file: JFile): Boolean =
   140     state.change_result(st =>
   141       st.models.get(file) match {
   142         case None => (false, st)
   143         case Some(model) => (true, st.update_models(Some(file -> model.external(true))))
   144       })
   145 
   146   def sync_models(changed_files: Set[JFile]): Unit =
   147     state.change(st =>
   148       {
   149         val changed_models =
   150           (for {
   151             (file, model) <- st.models.iterator
   152             if changed_files(file) && model.external_file
   153             text <- read_file_content(file)
   154             model1 <- model.change_text(text)
   155           } yield (file, model1)).toList
   156         st.update_models(changed_models)
   157       })
   158 
   159 
   160   /* resolve dependencies */
   161 
   162   def resolve_dependencies(session: Session, file_watcher: File_Watcher): (Boolean, Boolean) =
   163   {
   164     state.change_result(st =>
   165       {
   166         /* theory files */
   167 
   168         val thys =
   169           (for ((_, model) <- st.models.iterator if model.is_theory)
   170            yield (model.node_name, Position.none)).toList
   171 
   172         val thy_files = thy_info.dependencies(thys).deps.map(_.name)
   173 
   174 
   175         /* auxiliary files */
   176 
   177         val stable_tip_version =
   178           if (st.models.forall(entry => entry._2.is_stable))
   179             session.current_state().stable_tip_version
   180           else None
   181 
   182         val aux_files =
   183           stable_tip_version match {
   184             case Some(version) => undefined_blobs(version.nodes)
   185             case None => Nil
   186           }
   187 
   188 
   189         /* loaded models */
   190 
   191         val loaded_models =
   192           (for {
   193             node_name <- thy_files.iterator ++ aux_files.iterator
   194             file = node_file(node_name)
   195             if !st.models.isDefinedAt(file)
   196             text <- { file_watcher.register_parent(file); read_file_content(file) }
   197           }
   198           yield {
   199             val model = Document_Model.init(session, node_name)
   200             val model1 = (model.change_text(text) getOrElse model).external(true)
   201             (file, model1)
   202           }).toList
   203 
   204         val invoke_input = loaded_models.nonEmpty
   205         val invoke_load = stable_tip_version.isEmpty
   206 
   207         ((invoke_input, invoke_load), st.update_models(loaded_models))
   208       })
   209   }
   210 
   211 
   212   /* pending input */
   213 
   214   def flush_input(session: Session)
   215   {
   216     state.change(st =>
   217       {
   218         val changed_models =
   219           (for {
   220             file <- st.pending_input.iterator
   221             model <- st.models.get(file)
   222             (edits, model1) <- model.flush_edits(st.document_blobs)
   223           } yield (edits, (file, model1))).toList
   224 
   225         session.update(st.document_blobs, changed_models.flatMap(_._1))
   226         st.copy(
   227           models = st.models ++ changed_models.iterator.map(_._2),
   228           pending_input = Set.empty)
   229       })
   230   }
   231 
   232 
   233   /* pending output */
   234 
   235   def update_output(changed_nodes: Traversable[JFile]): Unit =
   236     state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes))
   237 
   238   def flush_output(channel: Channel): Boolean =
   239   {
   240     state.change_result(st =>
   241       {
   242         val (postponed, flushed) =
   243           (for {
   244             file <- st.pending_output.iterator
   245             model <- st.models.get(file)
   246           } yield (file, model, model.rendering())).toList.partition(_._3.snapshot.is_outdated)
   247 
   248         val changed_iterator =
   249           for {
   250             (file, model, rendering) <- flushed.iterator
   251             (changed_diags, changed_decos, model1) = model.publish(rendering)
   252             if changed_diags.isDefined || changed_decos.isDefined
   253           }
   254           yield {
   255             for (diags <- changed_diags)
   256               channel.write(Protocol.PublishDiagnostics(file, rendering.diagnostics_output(diags)))
   257             if (pide_extensions) {
   258               for (decos <- changed_decos; deco <- decos)
   259                 channel.write(rendering.decoration_output(deco).json(file))
   260             }
   261             (file, model1)
   262           }
   263 
   264         (postponed.nonEmpty,
   265           st.copy(
   266             models = st.models ++ changed_iterator,
   267             pending_output = postponed.map(_._1).toSet))
   268       }
   269     )
   270   }
   271 
   272 
   273   /* output text */
   274 
   275   def output_text(s: String): String =
   276     if (unicode_symbols) Symbol.decode(s) else Symbol.encode(s)
   277 
   278   def output_xml(xml: XML.Tree): String =
   279     output_text(XML.content(xml))
   280 
   281   def output_pretty(body: XML.Body, margin: Int): String =
   282     output_text(Pretty.string_of(body, margin))
   283   def output_pretty_tooltip(body: XML.Body): String = output_pretty(body, tooltip_margin)
   284   def output_pretty_message(body: XML.Body): String = output_pretty(body, message_margin)
   285 
   286 
   287   /* caret handling */
   288 
   289   def update_caret(caret: Option[(JFile, Line.Position)])
   290   { state.change(_.copy(caret = caret)) }
   291 
   292   def caret_offset(): Option[(Document_Model, Text.Offset)] =
   293   {
   294     val st = state.value
   295     for {
   296       (file, pos) <- st.caret
   297       model <- st.models.get(file)
   298       offset <- model.content.doc.offset(pos)
   299     }
   300     yield (model, offset)
   301   }
   302 
   303 
   304   /* spell checker */
   305 
   306   val spell_checker = new Spell_Checker_Variable
   307   spell_checker.update(options)
   308 }