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