Kotlin

qlbf 的博客真的支持 Kotlin 的高亮吗?

qlbf 的博客真的支持 Kotlin 的高亮吗?

class Abcd<T>(val clazz: Class<T>) {
  fun printGenericParameter() = clazz.canonicalName
  companion object {
    inline operator fun <reified T> invoke() = Abcd(T::class.java)

    @JvmStatic fun Array<String>.main() {
      val abcd = Abcd<LiceInjectionElement>()
      abcd.printGenericParameter().let(::println)
    }
  }
}

Colliot1/3/2018, 1:45:45 PM

fun main(args: Array<String>) {
  val list = object : ArrayList<String>(), Cloneable {
    override fun clone(): Any {
      return super<ArrayList>.clone()
    }
  }
  System.out.println(list)
}
run breaking@ {
  (0..20).forEach continuing@ {
    if (10 <= it) return@breaking
    println(it)
  }
}
infix fun Int.`+`(int: Int) = this * int
fun Array<String>.main() {
  println(1 `+` 10) // 输出 10
  println(1 + 10) // 输出 11
}

这些高亮在 qlbf 的博文里全部有问题。

Colliot1/3/2018, 1:47:18 PM

我也找不到更好的高亮插件了,我稍微写复杂点它就没法parse了。

Jekyll 能用的高亮插件我记得的有两个,当初研究 Agda 的时候折腾了下,结果全都不支持 Agda 。
Python 写的那个被抛弃了,我现在用的是 Rouge 。

ice10001/4/2018, 7:10:24 AM

我也找不到更好的高亮插件了,我稍微写复杂点它就没法parse了。

Jekyll 能用的高亮插件我记得的有两个,当初研究 Agda 的时候折腾了下,结果全都不支持 Agda 。
Python 写的那个被抛弃了,我现在用的是 Rouge 。

——ice1000

好吧,知乎的貌似也是个菜鸡……这篇专栏里的高亮也不对。

Colliot1/4/2018, 7:24:11 AM

让我们来试试高亮 Agda

{-# OPTIONS --without-K --rewriting #-}

open import lib.Basics
open import lib.types.Int
open import lib.types.Pi

module lib.types.Group where

-- 1-approximation of groups without higher coherence conditions.
record GroupStructure {i} (El : Type i) --(El-level : has-level 0 El)
  : Type i where
  constructor group-structure
  field
    ident  : El
    inv    : El → El
    comp   : El → El → El
    unit-l : ∀ a → comp ident a == a
    assoc  : ∀ a b c → comp (comp a b) c == comp a (comp b c)
    inv-l  : ∀ a → (comp (inv a) a) == ident

  ⊙El : Ptd i
  ⊙El = ⊙[ El , ident ]

  private
    infix 80 _⊙_
    _⊙_ = comp

  abstract
    inv-r  : ∀ g → g ⊙ inv g == ident
    inv-r g =
      g ⊙ inv g                           =⟨ ! `_mathjax_internal$ unit-l (g ⊙ inv g) ⟩
      ident ⊙ (g ⊙ inv g)                 =⟨ ! $]^$` inv-l (inv g) |in-ctx _⊙ (g ⊙ inv g) ⟩
      (inv (inv g) ⊙ inv g) ⊙ (g ⊙ inv g) =⟨ assoc (inv (inv g)) (inv g) (g ⊙ inv g) ⟩
      inv (inv g) ⊙ (inv g ⊙ (g ⊙ inv g)) =⟨ ! $ assoc (inv g) g (inv g) |in-ctx inv (inv g) ⊙_ ⟩
      inv (inv g) ⊙ ((inv g ⊙ g) ⊙ inv g) =⟨ inv-l g |in-ctx (λ h → inv (inv g) ⊙ (h ⊙ inv g)) ⟩
      inv (inv g) ⊙ (ident ⊙ inv g)       =⟨ unit-l (inv g) |in-ctx inv (inv g) ⊙_ ⟩
      inv (inv g) ⊙ inv g                 =⟨ inv-l (inv g) ⟩
      ident                               =∎

Colliot1/4/2018, 7:25:07 AM

让我们来试试高亮 Agda

{-# OPTIONS --without-K --rewriting #-}

open import lib.Basics
open import lib.types.Int
open import lib.types.Pi

module lib.types.Group where

-- 1-approximation of groups without higher coherence conditions.
record GroupStructure {i} (El : Type i) --(El-level : has-level 0 El)
  : Type i where
  constructor group-structure
  field
    ident  : El
    inv    : El → El
    comp   : El → El → El
    unit-l : ∀ a → comp ident a == a
    assoc  : ∀ a b c → comp (comp a b) c == comp a (comp b c)
    inv-l  : ∀ a → (comp (inv a) a) == ident

  ⊙El : Ptd i
  ⊙El = ⊙[ El , ident ]

  private
    infix 80 _⊙_
    _⊙_ = comp

  abstract
    inv-r  : ∀ g → g ⊙ inv g == ident
    inv-r g =
      g ⊙ inv g                           =⟨ ! `_mathjax_internal$ unit-l (g ⊙ inv g) ⟩
      ident ⊙ (g ⊙ inv g)                 =⟨ ! $]^$` inv-l (inv g) |in-ctx _⊙ (g ⊙ inv g) ⟩
      (inv (inv g) ⊙ inv g) ⊙ (g ⊙ inv g) =⟨ assoc (inv (inv g)) (inv g) (g ⊙ inv g) ⟩
      inv (inv g) ⊙ (inv g ⊙ (g ⊙ inv g)) =⟨ ! $ assoc (inv g) g (inv g) |in-ctx inv (inv g) ⊙_ ⟩
      inv (inv g) ⊙ ((inv g ⊙ g) ⊙ inv g) =⟨ inv-l g |in-ctx (λ h → inv (inv g) ⊙ (h ⊙ inv g)) ⟩
      inv (inv g) ⊙ (ident ⊙ inv g)       =⟨ unit-l (inv g) |in-ctx inv (inv g) ⊙_ ⟩
      inv (inv g) ⊙ inv g                 =⟨ inv-l (inv g) ⟩
      ident                               =∎

——Colliot

好吧,不行……这 PrismJS 貌似也是个菜鸡

Colliot1/4/2018, 7:26:18 AM

很明显你这垃圾也不支持我写的Kotlin代码,你看那些背景是白色的字符,是不是意思是说没过Tokenizer。

ice10001/10/2018, 11:27:49 AM

很明显你这垃圾也不支持我写的Kotlin代码,你看那些背景是白色的字符,是不是意思是说没过Tokenizer。

——ice1000

不是,支持的,它这个样式就是 operator 带白色背景……

Colliot1/10/2018, 4:02:56 PM

预览:

取消

其他地方

ice1000 回复了 TeX 的源码到底在哪里?

就是去掉那两个引号啊,只保留左边的那个竖线和文字的灰色

Colliot 回复了 我终于(可能)实现了本站的热更新……

我觉得正确的方式应该是手动给一个重启成功的信号,至少不至于让开头初始化的部分就挂了……不过初始化挂了,和初始化成功但是每次请求都挂,似乎也没多大区别。

Colliot 回复了 我终于(可能)实现了本站的热更新……

pm2 的 reload 功能好像不是很稳,重启有错也能重启。或者说这其实是运行时错误,pm2 不把它当成重启失败。

Colliot 回复了 TeX 的源码到底在哪里?

正确的引用样式是什么?

ice1000 回复了 TeX 的源码到底在哪里?

虎哥你这个quote的辣眼睛的两个引号什么时候可以弄掉啊。

ice1000 回复了 TeX 的源码到底在哪里?

这么写渲染居然没有出问题。 在格上,Kleene 不动点定理(Kleene's fixed point theorem)的内容是: 如果 (L, sqsubseteq) 是一个完备格,并且函数 f : L to L 是连续的,那么有:<br/>

athit{lfp}(f) = mathit{sup}(K(bot))

Colliot 回复了 TeX 的源码到底在哪里?

我可能找到了,在这里。Web 语言写的,该怎么让它发挥作用呢?

ice1000 回复了 为什么这里的 MathJax 会闪烁,而 StackExchange 的不会?

肯定啊。双缓冲是个很简单的东西嘛。。。

ice1000 回复了 bct水群卖弱控制不住了

你就是头号卖弱犯,踢了

nickname 回复了 PDF 格式的标准在哪里呢?

ISO 32000-1:2008, Document management -- Portable document format -- Part 1: PDF 1.7 Free to download provided Adobe: http://www.adobe.com/devnet/pdf/pdf_reference.html ISO 32000-2:2017, Document management -- Portable document format -- Part 2: PDF 2.0 Sell for CHF 198 (about ¥1318 Chinese Yuan) from ISO.org: https://www.iso.org/standard/63534.html