Searched refs:cmd (Results 1 - 25 of 58) sorted by relevance

123

/seL4-l4v-10.1.1/isabelle/src/Pure/Thy/
H A Dthy_syntax.scala127 def insert_text(cmd: Option[Command], text: String): Linear_Set[Command] =
128 if (text == "") commands else commands.insert_after(cmd, Command.text(text))
131 case (cmd, cmd_start) =>
132 e.can_edit(cmd.source, cmd_start) ||
133 e.is_insert && e.start == cmd_start + cmd.length
135 case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
136 val (rest, text) = e.edit(cmd.source, cmd_start)
137 val new_commands = insert_text(Some(cmd), text) - cmd
[all...]
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Thy/
H A Dthy_syntax.scala127 def insert_text(cmd: Option[Command], text: String): Linear_Set[Command] =
128 if (text == "") commands else commands.insert_after(cmd, Command.text(text))
131 case (cmd, cmd_start) =>
132 e.can_edit(cmd.source, cmd_start) ||
133 e.is_insert && e.start == cmd_start + cmd.length
135 case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
136 val (rest, text) = e.edit(cmd.source, cmd_start)
137 val new_commands = insert_text(Some(cmd), text) - cmd
[all...]
/seL4-l4v-10.1.1/HOL4/tools-poly/poly/
H A DMosml.sml7 fun run cmd args inp =
25 catenate (cmd :: List.@(args, ["<", infile, "1>", outfile,
28 (* catenate (cmd :: List.@(args, ["<", infile, "&>", outfile])) *)
34 handle IO.Io _ => Failure (cmd ^ ": command failed"))
/seL4-l4v-10.1.1/isabelle/src/Doc/Functions/document/
H A Dintro.tex22 Section 2 introduces the syntax and basic operation of the \cmd{fun}
26 Section 3 introduces the more verbose \cmd{function} command which
48 The new \cmd{function} command, and its short form \cmd{fun} have mostly
49 replaced the traditional \cmd{recdef} command \cite{slind-tfl}. They solve
50 a few of technical issues around \cmd{recdef}, and allow definitions
53 In addition there is also the \cmd{partial\_function} command
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Functions/document/
H A Dintro.tex22 Section 2 introduces the syntax and basic operation of the \cmd{fun}
26 Section 3 introduces the more verbose \cmd{function} command which
48 The new \cmd{function} command, and its short form \cmd{fun} have mostly
49 replaced the traditional \cmd{recdef} command \cite{slind-tfl}. They solve
50 a few of technical issues around \cmd{recdef}, and allow definitions
53 In addition there is also the \cmd{partial\_function} command
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/milawa-prover/
H A Dcore.lisp1497 (cmd state)
1500 (if (or (not (tuplep 2 cmd))
1501 (not (equal (first cmd) 'switch)))
1502 (error (list 'admit-switch 'invalid-cmd cmd))
1507 (name (second cmd)))
1517 (cmd state)
1520 (if (or (not (tuplep 4 cmd))
1521 (not (equal (first cmd) 'verify)))
1522 (error (list 'admit-theorem 'invalid-cmd cm
[all...]
/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/
H A DtttOpen.sml47 val cmd = String.concatWith " " [heapname_string,">",fileout] value
49 cmd_in_dir dir cmd;
62 val cmd = String.concatWith " " [cmd0,file',">",fileout] value
64 cmd_in_dir dir cmd;
79 val cmd = value
84 cmd_in_dir dir cmd
/seL4-l4v-10.1.1/l4v/misc/regression/
H A Dcpuusage.py125 cmd = repr(' '.join(self.proc.cmdline()))
127 cmd = '??'
128 warnings.warn("cpu non-monotonic: %.15f -> %.15f, pid=%d, cmd=%s" %
129 (self.cpu, total, self.pid, cmd),
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/
H A Dsimplifier_trace_dockable.scala90 case Some(cmd) =>
91 (snapshot, cmd, snapshot.command_results(cmd), cmd.id)
/seL4-l4v-10.1.1/isabelle/src/HOL/Mirabelle/lib/scripts/
H A Dmirabelle.pl162 my $cmd =
167 my $result = system "bash", "-c", $cmd;
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/
H A Dsimplifier_trace_dockable.scala90 case Some(cmd) =>
91 (snapshot, cmd, snapshot.command_results(cmd), cmd.id)
/seL4-l4v-10.1.1/l4v/isabelle/src/HOL/Mirabelle/lib/scripts/
H A Dmirabelle.pl162 my $cmd =
167 my $result = system "bash", "-c", $cmd;
/seL4-l4v-10.1.1/seL4/src/plat/tk1/machine/
H A Dsmmu.c149 uint32_t cmd = PTC_FLUSH_ALL; local
150 smmu_regs->smmu_ptc_flush = cmd;
156 uint32_t cmd = TLB_FLUSH_ALL; local
157 smmu_regs->smmu_tlb_flush = cmd;
/seL4-l4v-10.1.1/isabelle/src/Pure/PIDE/
H A Dquery_operation.scala79 case Some(cmd) =>
80 val snapshot = editor.node_snapshot(cmd.node_name)
81 val command_results = snapshot.command_results(cmd)
87 val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd)
H A Ddocument.scala158 def insert(cmd: Command, fn: String, args: List[String]): Overlays =
159 new Overlays(rep.insert(cmd, (fn, args)))
160 def remove(cmd: Command, fn: String, args: List[String]): Overlays =
161 new Overlays(rep.remove(cmd, (fn, args)))
249 commands.iterator.filter(cmd => cmd.blobs.nonEmpty).toList
273 case (cmd, start) => start + cmd.length <= i }
340 def command_start(cmd: Command): Option[Text.Offset] =
341 Node.Commands.starts(commands.iterator).find(_._1 == cmd)
[all...]
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/PIDE/
H A Dquery_operation.scala79 case Some(cmd) =>
80 val snapshot = editor.node_snapshot(cmd.node_name)
81 val command_results = snapshot.command_results(cmd)
87 val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd)
H A Ddocument.scala158 def insert(cmd: Command, fn: String, args: List[String]): Overlays =
159 new Overlays(rep.insert(cmd, (fn, args)))
160 def remove(cmd: Command, fn: String, args: List[String]): Overlays =
161 new Overlays(rep.remove(cmd, (fn, args)))
249 commands.iterator.filter(cmd => cmd.blobs.nonEmpty).toList
273 case (cmd, start) => start + cmd.length <= i }
340 def command_start(cmd: Command): Option[Text.Offset] =
341 Node.Commands.starts(commands.iterator).find(_._1 == cmd)
[all...]
/seL4-l4v-10.1.1/HOL4/polyml/basis/
H A DUnix.sml90 fun executeInEnv (cmd, args, env) =
95 val s = FileSys.stat cmd (* Raises SysErr if the file doesn't exist. *)
97 if not (FileSys.ST.isReg s) orelse not (FileSys.access(cmd, [FileSys.A_EXEC]))
119 Process.exece(cmd, OS.Path.file cmd :: args, env);
134 fun execute (cmd, args) =
135 executeInEnv(cmd, args, Posix.ProcEnv.environ())
H A DSignal.sml33 fun signal(s, cmd) =
36 case cmd of
/seL4-l4v-10.1.1/HOL4/src/HolQbf/
H A DHolQbfLib.sml12 val cmd = "squolem2 -c " ^ path ^ " >/dev/null 2>&1" value
14 Feedback.HOL_MESG ("HolQbfLib: calling external command '" ^ cmd ^ "'")
16 val _ = Systeml.system_ps cmd
/seL4-l4v-10.1.1/HOL4/tools/Holmake/
H A DHM_GraphBuildJ1.sml107 | cmd as (BuiltInCmd (BIC_BuildScript thyname)) =>
109 val others = find_nodes_by_command g cmd
115 | cmd as SomeCmd c =>
129 val others = find_nodes_by_command g cmd
H A DHolmake_types.sml56 fun extract_quotation0 cmd acc ss = let
61 val extract = extract_quotation0 cmd
74 #"#" => if not cmd then
78 if cmd then
196 val (cmd, rest) = splitAt(ss, i) value
198 val cmd = slice(cmd, 1, NONE) (* drop TAB *) value
200 docmds (extract_cmd_quotation cmd :: acc) rest
/seL4-l4v-10.1.1/isabelle/src/Pure/Isar/
H A Douter_syntax.scala174 case Some(cmd) =>
175 val name = cmd.source
177 (0 /: span.takeWhile(_ != cmd)) {
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Isar/
H A Douter_syntax.scala174 case Some(cmd) =>
175 val name = cmd.source
177 (0 /: span.takeWhile(_ != cmd)) {
/seL4-l4v-10.1.1/HOL4/src/HolSmt/
H A DSolverSpec.sml27 val cmd = cmd_stem ^ infile ^ " > " ^ outfile value
30 Feedback.HOL_MESG ("HolSmtLib: calling external command '" ^ cmd ^ "'")
32 val _ = Systeml.system_ps cmd

Completed in 130 milliseconds

123