1 files changed, 3 insertions, 134 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() {