src/Tools/VSCode/src/vscode_resources.scala
author wenzelm
Mon Sep 18 18:19:06 2017 +0200 (22 months ago)
changeset 66676 39db5bb7eb0a
parent 66674 30d5195299e2
child 66714 9fc4e144693c
permissions -rw-r--r--
recode Unicode text on the spot, e.g. from copy-paste of output;
     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     caret: Option[(JFile, Line.Position)] = None,
    24     overlays: Document.Overlays = Document.Overlays.empty,
    25     pending_input: Set[JFile] = Set.empty,
    26     pending_output: Set[JFile] = Set.empty)
    27   {
    28     def update_models(changed: Traversable[(JFile, Document_Model)]): State =
    29       copy(
    30         models = models ++ changed,
    31         pending_input = (pending_input /: changed) { case (set, (file, _)) => set + file },
    32         pending_output = (pending_output /: changed) { case (set, (file, _)) => set + file })
    33 
    34     def update_caret(new_caret: Option[(JFile, Line.Position)]): State =
    35       if (caret == new_caret) this
    36       else
    37         copy(
    38           caret = new_caret,
    39           pending_input = pending_input ++ caret.map(_._1) ++ new_caret.map(_._1))
    40 
    41     def get_caret(file: JFile): Option[Line.Position] =
    42       caret match {
    43         case Some((caret_file, caret_pos)) if caret_file == file => Some(caret_pos)
    44         case _ => None
    45       }
    46 
    47     lazy val document_blobs: Document.Blobs =
    48       Document.Blobs(
    49         (for {
    50           (_, model) <- models.iterator
    51           blob <- model.get_blob
    52         } yield (model.node_name -> blob)).toMap)
    53 
    54     def change_overlay(insert: Boolean, file: JFile,
    55         command: Command, fn: String, args: List[String]): State =
    56       copy(
    57         overlays =
    58           if (insert) overlays.insert(command, fn, args)
    59           else overlays.remove(command, fn, args),
    60         pending_input = pending_input + file)
    61   }
    62 
    63 
    64   /* caret */
    65 
    66   sealed case class Caret(file: JFile, model: Document_Model, offset: Text.Offset)
    67   {
    68     def node_name: Document.Node.Name = model.node_name
    69   }
    70 }
    71 
    72 class VSCode_Resources(
    73     val options: Options,
    74     session_base: Sessions.Base,
    75     log: Logger = No_Logger)
    76   extends Resources(session_base, log = log)
    77 {
    78   private val state = Synchronized(VSCode_Resources.State())
    79 
    80 
    81   /* options */
    82 
    83   def pide_extensions: Boolean = options.bool("vscode_pide_extensions")
    84   def unicode_symbols: Boolean = options.bool("vscode_unicode_symbols")
    85   def tooltip_margin: Int = options.int("vscode_tooltip_margin")
    86   def message_margin: Int = options.int("vscode_message_margin")
    87 
    88 
    89   /* document node name */
    90 
    91   def node_file(name: Document.Node.Name): JFile = new JFile(name.node)
    92 
    93   def node_name(file: JFile): Document.Node.Name =
    94     session_base.known.get_file(file, bootstrap = true) getOrElse {
    95       val node = file.getPath
    96       theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) match {
    97         case (true, theory) => Document.Node.Name.loaded_theory(theory)
    98         case (false, theory) =>
    99           val master_dir = if (theory == "") "" else file.getParent
   100           Document.Node.Name(node, master_dir, theory)
   101       }
   102     }
   103 
   104   override def append(dir: String, source_path: Path): String =
   105   {
   106     val path = source_path.expand
   107     if (dir == "" || path.is_absolute) File.platform_path(path)
   108     else if (path.is_current) dir
   109     else if (path.is_basic && !dir.endsWith("/") && !dir.endsWith(JFile.separator))
   110       dir + JFile.separator + File.platform_path(path)
   111     else if (path.is_basic) dir + File.platform_path(path)
   112     else File.absolute_name(new JFile(dir + JFile.separator + File.platform_path(path)))
   113   }
   114 
   115   def get_models: Map[JFile, Document_Model] = state.value.models
   116   def get_model(file: JFile): Option[Document_Model] = get_models.get(file)
   117   def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name))
   118 
   119 
   120   /* file content */
   121 
   122   def read_file_content(file: JFile): Option[String] =
   123     try { Some(Line.normalize(File.read(file))) }
   124     catch { case ERROR(_) => None }
   125 
   126   def get_file_content(file: JFile): Option[String] =
   127     get_model(file) match {
   128       case Some(model) => Some(model.content.text)
   129       case None => read_file_content(file)
   130     }
   131 
   132   override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
   133   {
   134     val file = node_file(name)
   135     get_model(file) match {
   136       case Some(model) => f(Scan.char_reader(model.content.text))
   137       case None if file.isFile =>
   138         val reader = Scan.byte_reader(file)
   139         try { f(reader) } finally { reader.close }
   140       case None =>
   141         error("No such file: " + quote(file.toString))
   142     }
   143   }
   144 
   145 
   146   /* document models */
   147 
   148   def visible_node(name: Document.Node.Name): Boolean =
   149     get_model(name) match {
   150       case Some(model) => model.node_visible
   151       case None => false
   152     }
   153 
   154   def change_model(
   155     session: Session,
   156     editor: Server.Editor,
   157     file: JFile,
   158     version: Long,
   159     text: String,
   160     range: Option[Line.Range] = None)
   161   {
   162     state.change(st =>
   163       {
   164         val model = st.models.getOrElse(file, Document_Model.init(session, editor, node_name(file)))
   165         val model1 =
   166           (model.change_text(text, range) getOrElse model).set_version(version).external(false)
   167         st.update_models(Some(file -> model1))
   168       })
   169   }
   170 
   171   def close_model(file: JFile): Boolean =
   172     state.change_result(st =>
   173       st.models.get(file) match {
   174         case None => (false, st)
   175         case Some(model) => (true, st.update_models(Some(file -> model.external(true))))
   176       })
   177 
   178   def sync_models(changed_files: Set[JFile]): Unit =
   179     state.change(st =>
   180       {
   181         val changed_models =
   182           (for {
   183             (file, model) <- st.models.iterator
   184             if changed_files(file) && model.external_file
   185             text <- read_file_content(file)
   186             model1 <- model.change_text(text)
   187           } yield (file, model1)).toList
   188         st.update_models(changed_models)
   189       })
   190 
   191 
   192   /* overlays */
   193 
   194   def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
   195     state.value.overlays(name)
   196 
   197   def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
   198     state.change(_.change_overlay(true, node_file(command.node_name), command, fn, args))
   199 
   200   def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
   201     state.change(_.change_overlay(false, node_file(command.node_name), command, fn, args))
   202 
   203 
   204   /* resolve dependencies */
   205 
   206   def resolve_dependencies(
   207     session: Session,
   208     editor: Server.Editor,
   209     file_watcher: File_Watcher): (Boolean, Boolean) =
   210   {
   211     state.change_result(st =>
   212       {
   213         /* theory files */
   214 
   215         val thys =
   216           (for ((_, model) <- st.models.iterator if model.is_theory)
   217            yield (model.node_name, Position.none)).toList
   218 
   219         val thy_files = thy_info.dependencies(thys).deps.map(_.name)
   220 
   221 
   222         /* auxiliary files */
   223 
   224         val stable_tip_version =
   225           if (st.models.forall(entry => entry._2.is_stable))
   226             session.current_state().stable_tip_version
   227           else None
   228 
   229         val aux_files =
   230           stable_tip_version match {
   231             case Some(version) => undefined_blobs(version.nodes)
   232             case None => Nil
   233           }
   234 
   235 
   236         /* loaded models */
   237 
   238         val loaded_models =
   239           (for {
   240             node_name <- thy_files.iterator ++ aux_files.iterator
   241             file = node_file(node_name)
   242             if !st.models.isDefinedAt(file)
   243             text <- { file_watcher.register_parent(file); read_file_content(file) }
   244           }
   245           yield {
   246             val model = Document_Model.init(session, editor, node_name)
   247             val model1 = (model.change_text(text) getOrElse model).external(true)
   248             (file, model1)
   249           }).toList
   250 
   251         val invoke_input = loaded_models.nonEmpty
   252         val invoke_load = stable_tip_version.isEmpty
   253 
   254         ((invoke_input, invoke_load), st.update_models(loaded_models))
   255       })
   256   }
   257 
   258 
   259   /* pending input */
   260 
   261   def flush_input(session: Session, channel: Channel)
   262   {
   263     state.change(st =>
   264       {
   265         val changed_models =
   266           (for {
   267             file <- st.pending_input.iterator
   268             model <- st.models.get(file)
   269             (edits, model1) <-
   270               model.flush_edits(unicode_symbols, st.document_blobs, file, st.get_caret(file))
   271           } yield (edits, (file, model1))).toList
   272 
   273         for { ((workspace_edits, _), _) <- changed_models if workspace_edits.nonEmpty }
   274           channel.write(Protocol.WorkspaceEdit(workspace_edits))
   275 
   276         session.update(st.document_blobs, changed_models.flatMap(res => res._1._2))
   277 
   278         st.copy(
   279           models = st.models ++ changed_models.iterator.map(_._2),
   280           pending_input = Set.empty)
   281       })
   282   }
   283 
   284 
   285   /* pending output */
   286 
   287   def update_output(changed_nodes: Traversable[JFile]): Unit =
   288     state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes))
   289 
   290   def update_output_visible(): Unit =
   291     state.change(st => st.copy(pending_output = st.pending_output ++
   292       (for ((file, model) <- st.models.iterator if model.node_visible) yield file)))
   293 
   294   def flush_output(channel: Channel): Boolean =
   295   {
   296     state.change_result(st =>
   297       {
   298         val (postponed, flushed) =
   299           (for {
   300             file <- st.pending_output.iterator
   301             model <- st.models.get(file)
   302           } yield (file, model, model.rendering())).toList.partition(_._3.snapshot.is_outdated)
   303 
   304         val changed_iterator =
   305           for {
   306             (file, model, rendering) <- flushed.iterator
   307             (changed_diags, changed_decos, model1) = model.publish(rendering)
   308             if changed_diags.isDefined || changed_decos.isDefined
   309           }
   310           yield {
   311             for (diags <- changed_diags)
   312               channel.write(Protocol.PublishDiagnostics(file, rendering.diagnostics_output(diags)))
   313             if (pide_extensions) {
   314               for (decos <- changed_decos; deco <- decos)
   315                 channel.write(rendering.decoration_output(deco).json(file))
   316             }
   317             (file, model1)
   318           }
   319 
   320         (postponed.nonEmpty,
   321           st.copy(
   322             models = st.models ++ changed_iterator,
   323             pending_output = postponed.map(_._1).toSet))
   324       }
   325     )
   326   }
   327 
   328 
   329   /* output text */
   330 
   331   def output_text(s: String): String =
   332     if (unicode_symbols) Symbol.decode(s) else Symbol.encode(s)
   333 
   334   def output_xml(xml: XML.Tree): String =
   335     output_text(XML.content(xml))
   336 
   337   def output_pretty(body: XML.Body, margin: Int): String =
   338     output_text(Pretty.string_of(body, margin))
   339   def output_pretty_tooltip(body: XML.Body): String = output_pretty(body, tooltip_margin)
   340   def output_pretty_message(body: XML.Body): String = output_pretty(body, message_margin)
   341 
   342 
   343   /* caret handling */
   344 
   345   def update_caret(caret: Option[(JFile, Line.Position)])
   346   { state.change(_.update_caret(caret)) }
   347 
   348   def get_caret(): Option[VSCode_Resources.Caret] =
   349   {
   350     val st = state.value
   351     for {
   352       (file, pos) <- st.caret
   353       model <- st.models.get(file)
   354       offset <- model.content.doc.offset(pos)
   355     }
   356     yield VSCode_Resources.Caret(file, model, offset)
   357   }
   358 
   359 
   360   /* spell checker */
   361 
   362   val spell_checker = new Spell_Checker_Variable
   363   spell_checker.update(options)
   364 }