src/Tools/VSCode/src/vscode_resources.scala
author wenzelm
Sun Jan 08 14:46:04 2017 +0100 (2017-01-08 ago)
changeset 64834 0a7179ad430d
parent 64833 0f410e3b1d20
child 64839 842163abfc0d
permissions -rw-r--r--
tuned;
     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   {
    26     lazy val document_blobs: Document.Blobs =
    27       Document.Blobs(
    28         (for {
    29           (_, model) <- models.iterator
    30           blob <- model.get_blob
    31         } yield (model.node_name -> blob)).toMap)
    32   }
    33 }
    34 
    35 class VSCode_Resources(
    36     val options: Options,
    37     val text_length: Text.Length,
    38     loaded_theories: Set[String],
    39     known_theories: Map[String, Document.Node.Name],
    40     base_syntax: Outer_Syntax,
    41     log: Logger = No_Logger)
    42   extends Resources(loaded_theories, known_theories, base_syntax, log)
    43 {
    44   private val state = Synchronized(VSCode_Resources.State())
    45 
    46 
    47   /* document node name */
    48 
    49   def node_file(name: Document.Node.Name): JFile = new JFile(name.node)
    50 
    51   def node_name(file: JFile): Document.Node.Name =
    52   {
    53     val node = file.getPath
    54     val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("")
    55     val master_dir = if (theory == "") "" else file.getParent
    56     Document.Node.Name(node, master_dir, theory)
    57   }
    58 
    59   override def append(dir: String, source_path: Path): String =
    60   {
    61     val path = source_path.expand
    62     if (dir == "" || path.is_absolute) File.platform_path(path)
    63     else if (path.is_current) dir
    64     else if (path.is_basic && !dir.endsWith("/") && !dir.endsWith(JFile.separator))
    65       dir + JFile.separator + File.platform_path(path)
    66     else if (path.is_basic) dir + File.platform_path(path)
    67     else new JFile(dir + JFile.separator + File.platform_path(path)).getCanonicalPath
    68   }
    69 
    70   def get_model(file: JFile): Option[Document_Model] = state.value.models.get(file)
    71   def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name))
    72 
    73 
    74   /* file content */
    75 
    76   def read_file_content(file: JFile): Option[String] =
    77     try { Some(Line.normalize(File.read(file))) }
    78     catch { case ERROR(_) => None }
    79 
    80   def get_file_content(file: JFile): Option[String] =
    81     get_model(file) match {
    82       case Some(model) => Some(model.content.text)
    83       case None => read_file_content(file)
    84     }
    85 
    86   def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
    87     for {
    88       (_, model) <- state.value.models.iterator
    89       Text.Info(range, entry) <- model.content.bibtex_entries.iterator
    90     } yield Text.Info(range, (entry, model))
    91 
    92   override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    93   {
    94     val file = node_file(name)
    95     get_model(file) match {
    96       case Some(model) => f(Scan.char_reader(model.content.text))
    97       case None if file.isFile =>
    98         val reader = Scan.byte_reader(file)
    99         try { f(reader) } finally { reader.close }
   100       case None =>
   101         error("No such file: " + quote(file.toString))
   102     }
   103   }
   104 
   105 
   106   /* document models */
   107 
   108   def visible_node(name: Document.Node.Name): Boolean =
   109     get_model(name) match {
   110       case Some(model) => model.node_visible
   111       case None => false
   112     }
   113 
   114   def update_model(session: Session, file: JFile, text: String)
   115   {
   116     state.change(st =>
   117       {
   118         val model = st.models.getOrElse(file, Document_Model.init(session, node_name(file)))
   119         val model1 = (model.update_text(text) getOrElse model).external(false)
   120         st.copy(
   121           models = st.models + (file -> model1),
   122           pending_input = st.pending_input + file)
   123       })
   124   }
   125 
   126   def close_model(file: JFile): Option[Document_Model] =
   127     state.change_result(st =>
   128       st.models.get(file) match {
   129         case None => (None, st)
   130         case Some(model) =>
   131           (Some(model), st.copy(models = st.models + (file -> model.external(true))))
   132       })
   133 
   134   def sync_models(changed_files: Set[JFile]): Boolean =
   135     state.change_result(st =>
   136       {
   137         val changed_models =
   138           (for {
   139             (file, model) <- st.models.iterator
   140             if changed_files(file) && model.external_file
   141             text <- read_file_content(file)
   142             model1 <- model.update_text(text)
   143           } yield (file, model1)).toList
   144         if (changed_models.isEmpty) (false, st)
   145         else (true,
   146           st.copy(
   147             models = (st.models /: changed_models)(_ + _),
   148             pending_input = (st.pending_input /: changed_models.iterator.map(_._1))(_ + _)))
   149       })
   150 
   151 
   152   /* resolve dependencies */
   153 
   154   val thy_info = new Thy_Info(this)
   155 
   156   def resolve_dependencies(session: Session, watcher: File_Watcher): (Boolean, Boolean) =
   157   {
   158     state.change_result(st =>
   159       {
   160         /* theory files */
   161 
   162         val thys =
   163           (for ((_, model) <- st.models.iterator if model.is_theory)
   164            yield (model.node_name, Position.none)).toList
   165 
   166         val thy_files = thy_info.dependencies("", thys).deps.map(_.name)
   167 
   168 
   169         /* auxiliary files */
   170 
   171         val stable_tip_version =
   172           if (st.models.forall(entry => entry._2.is_stable))
   173             session.current_state().stable_tip_version
   174           else None
   175 
   176         val aux_files =
   177           stable_tip_version match {
   178             case Some(version) => undefined_blobs(version.nodes)
   179             case None => Nil
   180           }
   181 
   182 
   183         /* loaded models */
   184 
   185         val loaded_models =
   186           (for {
   187             node_name <- thy_files.iterator ++ aux_files.iterator
   188             file = node_file(node_name)
   189             if !st.models.isDefinedAt(file)
   190             text <- { watcher.register_parent(file); read_file_content(file) }
   191           }
   192           yield {
   193             val model = Document_Model.init(session, node_name)
   194             val model1 = (model.update_text(text) getOrElse model).external(true)
   195             (file, model1)
   196           }).toList
   197 
   198         val invoke_input = loaded_models.nonEmpty
   199         val invoke_load = stable_tip_version.isEmpty
   200 
   201         ((invoke_input, invoke_load),
   202           st.copy(
   203             models = st.models ++ loaded_models,
   204             pending_input = st.pending_input ++ loaded_models.iterator.map(_._1)))
   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: List[JFile]): Unit =
   233     state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes))
   234 
   235   def flush_output(channel: Channel)
   236   {
   237     state.change(st =>
   238       {
   239         val changed_iterator =
   240           for {
   241             file <- st.pending_output.iterator
   242             model <- st.models.get(file)
   243             rendering = model.rendering()
   244             (diagnostics, model1) <- model.publish_diagnostics(rendering)
   245           } yield {
   246             channel.diagnostics(file, rendering.diagnostics_output(diagnostics))
   247             (file, model1)
   248           }
   249         st.copy(
   250           models = (st.models /: changed_iterator)(_ + _),
   251           pending_output = Set.empty)
   252       }
   253     )
   254   }
   255 }