better code structure for isabelle-proto

3 files changed, 148 insertions, 135 deletions

diff --git a/isabelle-proto/src/main.rs b/isabelle-proto/src/main.rs
index b16b8ac..535dd52 100644
--- a/isabelle-proto/src/main.rs
+++ b/isabelle-proto/src/main.rs
@@ -1,131 +1,20 @@
 
 mod session;
+mod messages;
 
 use regex::Regex;
 use serde::{Deserialize, Serialize, de::DeserializeOwned};
 use serde_json::{Result, Value};
 use session::IsabelleSession;
+use messages::*;
+
 
 use std::{io::{BufRead, BufReader, BufWriter, Write}, path::PathBuf, process::{ChildStdout, Command, Stdio}};
 use std::fmt::Debug;
 
-use isabelle_unicode::PrettyUnicode;
 
 use structopt::StructOpt;
 
-type SessionID = String;
-type TaskID = String;
-
-#[derive(Serialize, Deserialize)]
-#[serde(untagged)]
-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)]
-enum SyncAnswer<T,E> {
-    Ok (T),
-    Error (E),
-}
-
-enum AsyncAnswer<T, E, N> {
-    Finished (T),
-    Failed (E),
-    Note (N)
-}
-
-#[derive(Deserialize, Debug)]
-struct ClientHello {
-    isabelle_id : String,
-    isabelle_version : String
-}
-
-#[derive(Deserialize)]
-struct SessionStartedOk {
-    session_id : String,
-    tmp_dir : String,
-    task : String
-}
-
-#[derive(Deserialize)]
-struct SessionStartedNote {
-    percentage : u8,
-    task : TaskID,
-    message : String,
-    kind : String,
-    session : String,
-    theory : String
-}
-
-#[derive(Deserialize, Clone, Debug)]
-struct SessionStartedFinished {
-    session_id : SessionID,
-    tmp_dir : String,
-    task : TaskID
-}
-
-
-
-#[derive(Deserialize, Clone, Debug)]
-struct UseTheoriesFinished {
-    ok : bool,
-    errors : Vec<IsabelleError>,
-    nodes : Vec<IsabelleNode>,
-    task : TaskID,
-}
-
-#[derive(Deserialize, Clone, Debug)]
-struct IsabelleError {
-    kind : String,
-    message : String,
-    pos : Span
-}
-
-#[derive(Deserialize, Clone, Debug)]
-struct IsabelleNode {
-    messages : Vec<IsabelleError>,
-    exports : Vec<()>,
-    status : Status,
-    theory_name : String,
-    node_name : String
-}
-
-#[derive(Deserialize, Clone, Debug)]
-struct Status {
-    percentage : u8,
-    unprocessed : u64,
-    running : u64,
-    finished : u64,
-    failed : u64,
-    total : u64,
-    consolidated : bool,
-    canceled : bool,
-    ok : bool,
-    warned : u64
-}
-
-#[derive(Deserialize,Clone, Debug)]
-struct Span {
-    line : u64,
-    offset : u64,
-    end_offset : u64,
-    file : String
-}
-
-#[derive(Deserialize)]
-struct AsyncStartOk {
-    task : TaskID
-}
 
 fn decode_sync<'a, T> (msg: &'a str) -> Option<SyncAnswer<T, String>>
 where T: Deserialize<'a> {
@@ -158,26 +47,6 @@ where T: Deserialize<'a>, N: Deserialize<'a>, E: Deserialize<'a> {
 
 
 
-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
-    }
-}
 
 fn wait_for_client(pipe: &mut BufReader<ChildStdout>) -> Option<ClientHello> {
     for res in pipe.lines() {
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
+    }
+}
diff --git a/isabelle-proto/src/session.rs b/isabelle-proto/src/session.rs
index 85081d4..11fb5bc 100644
--- a/isabelle-proto/src/session.rs
+++ b/isabelle-proto/src/session.rs
@@ -4,8 +4,9 @@ use regex::Regex;
 use serde::de::DeserializeOwned;
 use serde_json::Value;
 
-use crate::{AsyncAnswer, ClientCommand, Encode, SessionStartedFinished, UseTheoriesFinished, decode_async, get_async_task_id, wait_for_client};
+use crate::messages::*;
 
+use crate::{decode_async, get_async_task_id, wait_for_client};