/seL4-l4v-10.1.1/isabelle/src/Pure/Thy/ |
H A D | thy_syntax.scala | 127 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 D | thy_syntax.scala | 127 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 D | Mosml.sml | 7 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 D | intro.tex | 22 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 D | intro.tex | 22 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 D | core.lisp | 1497 (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 D | tttOpen.sml | 47 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 D | cpuusage.py | 125 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 D | simplifier_trace_dockable.scala | 90 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 D | mirabelle.pl | 162 my $cmd = 167 my $result = system "bash", "-c", $cmd;
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/ |
H A D | simplifier_trace_dockable.scala | 90 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 D | mirabelle.pl | 162 my $cmd = 167 my $result = system "bash", "-c", $cmd;
|
/seL4-l4v-10.1.1/seL4/src/plat/tk1/machine/ |
H A D | smmu.c | 149 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 D | query_operation.scala | 79 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 D | document.scala | 158 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 D | query_operation.scala | 79 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 D | document.scala | 158 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 D | Unix.sml | 90 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 D | Signal.sml | 33 fun signal(s, cmd) = 36 case cmd of
|
/seL4-l4v-10.1.1/HOL4/src/HolQbf/ |
H A D | HolQbfLib.sml | 12 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 D | HM_GraphBuildJ1.sml | 107 | 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 D | Holmake_types.sml | 56 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 D | outer_syntax.scala | 174 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 D | outer_syntax.scala | 174 case Some(cmd) => 175 val name = cmd.source 177 (0 /: span.takeWhile(_ != cmd)) {
|
/seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
H A D | SolverSpec.sml | 27 val cmd = cmd_stem ^ infile ^ " > " ^ outfile value 30 Feedback.HOL_MESG ("HolSmtLib: calling external command '" ^ cmd ^ "'") 32 val _ = Systeml.system_ps cmd
|