isabelle_client/client/
args.rs

1use serde::{Deserialize, Serialize};
2/// Arguments for `cancel` command
3#[derive(Deserialize, Serialize, Debug)]
4pub struct CancelArgs {
5    /// Id of the task to try to cancel
6    pub task: String,
7}
8
9/// Arguments for `session_build` and `session_start` commands
10#[derive(Deserialize, Serialize, Default, Debug)]
11pub struct SessionBuildArgs {
12    /// Specifies the target session name. The build process will produce all required ancestor images according to the overall session graph.
13    pub session: String,
14    /// Environment of Isabelle system options is determined from preferences
15    #[serde(skip_serializing_if = "Option::is_none")]
16    pub preferences: Option<String>,
17    /// List of individual updates to the Isabelle system environment of the form `name=value` or `name`.
18    #[serde(skip_serializing_if = "Option::is_none")]
19    pub options: Option<Vec<String>>,
20    /// Specifies additional directories for session `ROOT`and `ROOTS` files
21    #[serde(skip_serializing_if = "Option::is_none")]
22    pub dirs: Option<Vec<String>>,
23    /// Specifies sessions whose theories should be included in the overall name space of session-qualified theory names.
24    /// Corresponds to `session` specification in `ROOT` files.
25    #[serde(skip_serializing_if = "Vec::is_empty")]
26    pub include_sessions: Vec<String>,
27}
28
29impl SessionBuildArgs {
30    pub fn session(session: &str) -> Self {
31        Self {
32            session: session.to_string(),
33            ..Default::default()
34        }
35    }
36}
37
38/// Arguments for `session_stop` command
39#[derive(Deserialize, Serialize, Debug)]
40pub struct SessionStopArgs {
41    /// Id of the session to stop
42    pub session_id: String,
43}
44
45/// Arguments for `use_theories` command
46#[derive(Deserialize, Serialize, Debug, Default)]
47pub struct UseTheoriesArgs {
48    pub session_id: String,
49    pub theories: Vec<String>,
50    #[serde(skip_serializing_if = "Option::is_none")]
51    pub master_dir: Option<String>,
52    #[serde(skip_serializing_if = "Option::is_none")]
53    pub unicode_symbols: Option<bool>,
54    #[serde(skip_serializing_if = "Option::is_none")]
55    pub export_pattern: Option<String>,
56    #[serde(skip_serializing_if = "Option::is_none")]
57    pub check_delay: Option<f64>,
58    #[serde(skip_serializing_if = "Option::is_none")]
59    pub check_limit: Option<usize>,
60    #[serde(skip_serializing_if = "Option::is_none")]
61    pub watchdog_timeout: Option<f64>,
62    #[serde(skip_serializing_if = "Option::is_none")]
63    pub nodes_status_delay: Option<f64>,
64}
65
66impl UseTheoriesArgs {
67    pub fn for_session(session_id: &str, theories: &[&str]) -> Self {
68        Self {
69            session_id: session_id.to_string(),
70            theories: theories.iter().map(|t| t.to_string()).collect(),
71            ..Default::default()
72        }
73    }
74}
75
76/// Arguments for `purge_theories` command
77#[derive(Deserialize, Serialize, Debug, Default)]
78pub struct PurgeTheoryArgs {
79    pub session_id: String,
80    pub theories: Vec<String>,
81    #[serde(skip_serializing_if = "Option::is_none")]
82    pub master_dir: Option<String>,
83    #[serde(skip_serializing_if = "Option::is_none")]
84    pub all: Option<bool>,
85}
86
87impl PurgeTheoryArgs {
88    pub fn for_session(session_id: &str, theories: &[&str]) -> Self {
89        Self {
90            session_id: session_id.to_string(),
91            theories: theories.iter().map(|t| t.to_string()).collect(),
92            ..Default::default()
93        }
94    }
95}
isabelle_client/client/args.rs

isabelle_client/client/
args.rs
