src/Pure/Thy/thy_resources.scala
author wenzelm
Sun, 12 Nov 2017 20:50:24 +0100
changeset 67063 10d608cc7470
parent 67062 ee0823ce2828
child 67064 fb487246ef4f
permissions -rw-r--r--
clarified modules;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
67054
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Thy/thy_resources.scala
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
     3
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
     4
PIDE resources for theory files.
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
     5
*/
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
     6
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
     7
package isabelle
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
     8
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
     9
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
    10
object Thy_Resources
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
    11
{
67061
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    12
  /* PIDE session */
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    13
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    14
  def start_session(
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    15
    options: Options,
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    16
    session_name: String,
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    17
    session_dirs: List[Path] = Nil,
67062
ee0823ce2828 optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents: 67061
diff changeset
    18
    session_base: Option[Sessions.Base] = None,
67061
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    19
    modes: List[String] = Nil,
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    20
    log: Logger = No_Logger): Session =
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    21
  {
67062
ee0823ce2828 optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents: 67061
diff changeset
    22
    val base =
ee0823ce2828 optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents: 67061
diff changeset
    23
      session_base getOrElse
ee0823ce2828 optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents: 67061
diff changeset
    24
        Sessions.base_info(options, session_name, dirs = session_dirs).check_base
ee0823ce2828 optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents: 67061
diff changeset
    25
    val resources = new Thy_Resources(base, log = log)
67061
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    26
    val session = new Session(options, resources)
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    27
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    28
    val session_error = Future.promise[String]
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    29
    var session_phase: Session.Consumer[Session.Phase] = null
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    30
    session_phase =
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    31
      Session.Consumer(getClass.getName) {
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    32
        case Session.Ready =>
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    33
          session.phase_changed -= session_phase
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    34
          session_error.fulfill("")
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    35
        case Session.Terminated(result) if !result.ok =>
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    36
          session.phase_changed -= session_phase
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    37
          session_error.fulfill("Prover startup failed: return code " + result.rc)
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    38
        case _ =>
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    39
      }
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    40
    session.phase_changed += session_phase
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    41
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    42
    Isabelle_Process.start(session, options,
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    43
      logic = session_name, dirs = session_dirs, modes = modes)
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    44
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    45
    session_error.join match {
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    46
      case "" => session
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    47
      case msg => session.stop(); error(msg)
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    48
    }
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    49
  }
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    50
67063
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
    51
  class Session private[Thy_Resources](
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
    52
    options: Options, override val resources: Thy_Resources)
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
    53
    extends isabelle.Session(options, resources)
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
    54
  {
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
    55
    session =>
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
    56
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
    57
    def load_theories(theories: List[(String, Position.T)],
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
    58
        qualifier: String = Sessions.DRAFT, master_dir: String = ""): List[Document.Node.Name] =
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
    59
      resources.load_theories(session, theories, qualifier = qualifier, master_dir = master_dir)
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
    60
  }
10d608cc7470 clarified modules;
wenzelm
parents: 67062
diff changeset
    61
67061
2efa25302f34 synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents: 67059
diff changeset
    62
67054
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
    63
  /* internal state */
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
    64
67058
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
    65
  sealed case class State(theories: Map[Document.Node.Name, Theory] = Map.empty)
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
    66
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
    67
  final class Theory private[Thy_Resources](
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
    68
    val node_name: Document.Node.Name,
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
    69
    val node_header: Document.Node.Header,
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
    70
    val text: String)
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
    71
  {
67058
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
    72
    override def toString: String = node_name.toString
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
    73
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
    74
    def node_perspective: Document.Node.Perspective_Text =
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
    75
      Document.Node.Perspective(true, Text.Perspective.full, Document.Node.Overlays.empty)
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
    76
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
    77
    def node_edits(old: Option[Theory]): List[Document.Edit_Text] =
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
    78
    {
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
    79
      val text_edits =
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
    80
        if (old.isEmpty) Text.Edit.inserts(0, text)
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
    81
        else Text.Edit.replace(0, old.get.text, text)
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
    82
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
    83
      if (text_edits.isEmpty) Nil
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
    84
      else
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
    85
        List(node_name -> Document.Node.Deps(node_header),
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
    86
          node_name -> Document.Node.Edits(text_edits),
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
    87
          node_name -> node_perspective)
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
    88
    }
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
    89
  }
67054
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
    90
}
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
    91
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
    92
class Thy_Resources(session_base: Sessions.Base, log: Logger = No_Logger)
67054
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
    93
  extends Resources(session_base, log = log)
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
    94
{
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
    95
  resources =>
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
    96
67054
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
    97
  private val state = Synchronized(Thy_Resources.State())
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
    98
67058
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
    99
  def read_thy(node_name: Document.Node.Name): Thy_Resources.Theory =
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   100
  {
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   101
    val path = node_name.path
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   102
    if (!node_name.is_theory) error("Not a theory file: " + path)
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   103
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   104
    val text = File.read(path)
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   105
    val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text))
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   106
    new Thy_Resources.Theory(node_name, node_header, text)
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   107
  }
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   108
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   109
  def load_theories(
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   110
    session: Session,
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   111
    theories: List[(String, Position.T)],
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   112
    qualifier: String = Sessions.DRAFT,
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   113
    master_dir: String = ""): List[Document.Node.Name] =
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   114
  {
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   115
    val import_names =
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   116
      for ((thy, pos) <- theories)
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   117
      yield (import_name(qualifier, master_dir, thy), pos)
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   118
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   119
    val dependencies = resources.dependencies(import_names).check_errors
67059
df7d728103f1 tuned signature;
wenzelm
parents: 67058
diff changeset
   120
    val loaded_theories = dependencies.theories.map(read_thy(_))
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   121
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   122
    val edits =
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   123
      state.change_result(st =>
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   124
      {
67058
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   125
        val theory_edits =
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   126
          for {
67058
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   127
            theory <- loaded_theories
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   128
            node_name = theory.node_name
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   129
            edits = theory.node_edits(st.theories.get(node_name))
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   130
            if edits.nonEmpty
67058
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   131
          } yield ((node_name, theory), edits)
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   132
67058
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   133
        val st1 = st.copy(theories = st.theories ++ theory_edits.map(_._1))
03d4954c68bb simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents: 67057
diff changeset
   134
        (theory_edits.flatMap(_._2), st1)
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   135
      })
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   136
    session.update(Document.Blobs.empty, edits)
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   137
67059
df7d728103f1 tuned signature;
wenzelm
parents: 67058
diff changeset
   138
    dependencies.theories
67056
e35ae3eeec93 load theories via PIDE document update;
wenzelm
parents: 67054
diff changeset
   139
  }
67054
9498b7522a99 PIDE resources for theory files;
wenzelm
parents:
diff changeset
   140
}