1 files changed, 143 insertions, 0 deletions
diff --git a/isabelle-proto/src/messages.rs b/isabelle-proto/src/messages.rs
new file mode 100644
index 0000000..908ddf1
--- /dev/null
+++ b/isabelle-proto/src/messages.rs
@@ -0,0 +1,143 @@
+
+use serde::{Deserialize, Serialize};
+
+pub type SessionID = String;
+pub type TaskID = String;
+
+#[derive(Serialize, Deserialize)]
+#[serde(untagged)]
+pub enum ClientCommand {
+    UseTheories {
+        session_id : SessionID,
+        theories : Vec<String>,
+        master_dir : Option<String>
+    },
+    SessionStart {
+        session : String,
+        include_sessions : Vec<String>
+    },
+    Echo (String),
+    ShutDown
+}
+
+#[derive(Debug)]
+pub enum SyncAnswer<T,E> {
+    Ok (T),
+    Error (E),
+}
+
+pub enum AsyncAnswer<T, E, N> {
+    Finished (T),
+    Failed (E),
+    Note (N)
+}
+
+#[derive(Deserialize, Debug)]
+pub struct ClientHello {
+    pub isabelle_id : String,
+    pub isabelle_version : String
+}
+
+#[allow(dead_code)]
+#[derive(Deserialize)]
+pub struct SessionStartedOk {
+    pub session_id : String,
+    pub tmp_dir : String,
+    pub task : String
+}
+
+#[allow(dead_code)]
+#[derive(Deserialize)]
+pub struct SessionStartedNote {
+    pub percentage : u8,
+    pub task : TaskID,
+    pub message : String,
+    pub kind : String,
+    pub session : String,
+    pub theory : String
+}
+
+#[derive(Deserialize, Clone, Debug)]
+pub struct SessionStartedFinished {
+    pub session_id : SessionID,
+    pub tmp_dir : String,
+    pub task : TaskID
+}
+
+
+
+#[derive(Deserialize, Clone, Debug)]
+pub struct UseTheoriesFinished {
+    pub ok : bool,
+    pub errors : Vec<IsabelleError>,
+    pub nodes : Vec<IsabelleNode>,
+    pub task : TaskID,
+}
+
+#[derive(Deserialize, Clone, Debug)]
+pub struct IsabelleError {
+    pub kind : String,
+    pub message : String,
+    pub pos : Span
+}
+
+#[derive(Deserialize, Clone, Debug)]
+pub struct IsabelleNode {
+    pub messages : Vec<IsabelleError>,
+    pub exports : Vec<()>,
+    pub status : Status,
+    pub theory_name : String,
+    pub node_name : String
+}
+
+#[derive(Deserialize, Clone, Debug)]
+pub struct Status {
+    pub percentage : u8,
+    pub unprocessed : u64,
+    pub running : u64,
+    pub finished : u64,
+    pub failed : u64,
+    pub total : u64,
+    pub consolidated : bool,
+    pub canceled : bool,
+    pub ok : bool,
+    pub warned : u64
+}
+
+#[derive(Deserialize,Clone, Debug)]
+pub struct Span {
+    pub line : u64,
+    pub offset : u64,
+    pub end_offset : u64,
+    pub file : String
+}
+
+#[derive(Deserialize)]
+pub struct AsyncStartOk {
+    pub task : TaskID
+}
+
+
+
+
+
+pub trait Encode {
+    fn encode (&self) -> String;
+}
+
+impl Encode for ClientCommand {
+    fn encode (&self) -> String {
+        let ty = match self {
+            ClientCommand::UseTheories {..} => "use_theories",
+            ClientCommand::SessionStart {..} => "session_start",
+            ClientCommand::Echo (..) => "echo",
+            ClientCommand::ShutDown => "shutdown"
+        };
+
+        let blob = serde_json::to_string(self).unwrap();
+
+        let res = ty.to_owned() + &blob + "\n";
+        println!("encoded: {}", res);
+        res
+    }
+}