src/Tools/VSCode/src/vscode_resources.scala
author wenzelm
Tue Jan 03 14:17:03 2017 +0100 (2017-01-03)
changeset 64759 100941134718
parent 64754 74d8793feceb
child 64766 6fd05caf55f0
permissions -rw-r--r--
clarified master_dir: file-URL;
     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, CharSequenceReader}
    15 
    16 
    17 object VSCode_Resources
    18 {
    19   /* internal state */
    20 
    21   sealed case class State(
    22     models: Map[String, Document_Model] = Map.empty,
    23     pending_input: Set[String] = Set.empty,
    24     pending_output: Set[String] = Set.empty)
    25 }
    26 
    27 class VSCode_Resources(
    28     val options: Options,
    29     val text_length: Text.Length,
    30     loaded_theories: Set[String],
    31     known_theories: Map[String, Document.Node.Name],
    32     base_syntax: Outer_Syntax,
    33     log: Logger = No_Logger)
    34   extends Resources(loaded_theories, known_theories, base_syntax, log)
    35 {
    36   private val state = Synchronized(VSCode_Resources.State())
    37 
    38 
    39   /* document node name */
    40 
    41   def node_name(uri: String): Document.Node.Name =
    42   {
    43     val theory = Thy_Header.thy_name_bootstrap(uri).getOrElse("")
    44     val master_dir =
    45       if (!Url.is_wellformed_file(uri) || theory == "") ""
    46       else Thy_Header.dir_name(uri)
    47     Document.Node.Name(uri, master_dir, theory)
    48   }
    49 
    50   override def append(dir: String, source_path: Path): String =
    51   {
    52     val path = source_path.expand
    53     if (path.is_absolute) "file://" + path.implode
    54     else if (dir == "") "file://" + (File.pwd() + path).implode
    55     else if (path.is_current) dir
    56     else Url.normalize_file(dir + "/" + path.implode)
    57   }
    58 
    59   override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    60   {
    61     val uri = name.node
    62     get_model(uri) match {
    63       case Some(model) =>
    64         val reader = new CharSequenceReader(model.doc.make_text)
    65         f(reader)
    66 
    67       case None =>
    68         val file = Url.file(uri)
    69         if (!file.isFile) error("No such file: " + quote(file.toString))
    70 
    71         val reader = Scan.byte_reader(file)
    72         try { f(reader) } finally { reader.close }
    73     }
    74   }
    75 
    76 
    77   /* document models */
    78 
    79   def get_model(uri: String): Option[Document_Model] = state.value.models.get(uri)
    80 
    81   def update_model(session: Session, uri: String, text: String)
    82   {
    83     state.change(st =>
    84       {
    85         val model = st.models.getOrElse(uri, Document_Model.init(session, uri))
    86         val model1 = (model.update_text(text) getOrElse model).external(false)
    87         st.copy(
    88           models = st.models + (uri -> model1),
    89           pending_input = st.pending_input + uri)
    90       })
    91   }
    92 
    93   def close_model(uri: String): Option[Document_Model] =
    94     state.change_result(st =>
    95       st.models.get(uri) match {
    96         case None => (None, st)
    97         case Some(model) =>
    98           (Some(model), st.copy(models = st.models + (uri -> model.external(true))))
    99       })
   100 
   101   def sync_models(changed_files: Set[JFile]): Boolean =
   102     state.change_result(st =>
   103       {
   104         val changed_models =
   105           (for {
   106             (uri, model) <- st.models.iterator
   107             if changed_files(model.file)
   108             model1 <- model.update_file
   109           } yield (uri, model1)).toList
   110         if (changed_models.isEmpty) (false, st)
   111         else (true,
   112           st.copy(
   113             models = (st.models /: changed_models)(_ + _),
   114             pending_input = (st.pending_input /: changed_models.iterator.map(_._1))(_ + _)))
   115       })
   116 
   117 
   118   /* resolve dependencies */
   119 
   120   val thy_info = new Thy_Info(this)
   121 
   122   def resolve_dependencies(session: Session): Boolean =
   123   {
   124     state.change_result(st =>
   125       {
   126         val thys =
   127           (for ((_, model) <- st.models.iterator if model.is_theory)
   128            yield (model.node_name, Position.none)).toList
   129 
   130         val loaded_models =
   131           (for {
   132             dep <- thy_info.dependencies("", thys).deps.iterator
   133             uri = dep.name.node
   134             if !st.models.isDefinedAt(uri)
   135             text <-
   136               try { Some(File.read(Url.file(uri))) }
   137               catch { case ERROR(_) => None }
   138           }
   139           yield {
   140             val model = Document_Model.init(session, uri)
   141             val model1 = (model.update_text(text) getOrElse model).external(true)
   142             (uri, model1)
   143           }).toList
   144 
   145         if (loaded_models.isEmpty) (false, st)
   146         else
   147           (true,
   148             st.copy(
   149               models = st.models ++ loaded_models,
   150               pending_input = st.pending_input ++ loaded_models.iterator.map(_._1)))
   151       })
   152   }
   153 
   154 
   155   /* pending input */
   156 
   157   def flush_input(session: Session)
   158   {
   159     state.change(st =>
   160       {
   161         val changed_models =
   162           (for {
   163             uri <- st.pending_input.iterator
   164             model <- st.models.get(uri)
   165             res <- model.flush_edits
   166           } yield res).toList
   167 
   168         session.update(Document.Blobs.empty, changed_models.flatMap(_._1))
   169         st.copy(
   170           models = (st.models /: changed_models) { case (ms, (_, m)) => ms + (m.uri -> m) },
   171           pending_input = Set.empty)
   172       })
   173   }
   174 
   175 
   176   /* pending output */
   177 
   178   def update_output(changed_nodes: List[String]): Unit =
   179     state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes))
   180 
   181   def flush_output(channel: Channel)
   182   {
   183     state.change(st =>
   184       {
   185         val changed_iterator =
   186           for {
   187             uri <- st.pending_output.iterator
   188             model <- st.models.get(uri)
   189             rendering = model.rendering()
   190             (diagnostics, model1) <- model.publish_diagnostics(rendering)
   191           } yield {
   192             channel.diagnostics(model1.uri, rendering.diagnostics_output(diagnostics))
   193             model1
   194           }
   195         st.copy(
   196           models = (st.models /: changed_iterator) { case (ms, m) => ms + (m.uri -> m) },
   197           pending_output = Set.empty)
   198       }
   199     )
   200   }
   201 }